Email Gateway (Aug 23 2022 at 08:18): Email Gateway (Aug 23 2022 at 08:18):From: Makarius <makarius@sketis.net>
The grammar above does not provide any production to introduce f1, so there is
no way to parse that.
The hard crash with an exception is a brutal way to say that -- there should
be a regular syntax error instead.
This used to work in Isabelle2017, while Isabelle2018 has the exception, see
also Isabelle/add9a9f6a290.
I have now made it more robust again for Isabelle2020-RC1:
https://isabelle-dev.sketis.net/rISABELLE53fcbede7bf7
Makarius
Last updated: Apr 26 2024 at 08:19 UTC