Email Gateway (Jan 16 2021 at 09:56): Email Gateway (Jan 16 2021 at 09:56):From: Stephan Merz <stephan.merz@loria.fr>
Dear list,
is it possible to retrieve a complete list of keywords / reserved words of, say, Isabelle/Pure, either from the sources or the documentation? (Appendix A of the Isar reference comes close but is not complete.) I understand that Isabelle's flexibility allows new syntax elements to be introduced, but having access to those that are present in Pure would be very helpful.
The background of my question is our use of Isabelle in the TLA+ Proof System where Isabelle input is auto-generated and we have to rename identifiers to avoid clashes with keywords. In ancient versions we retrieved that list from the Proof General emacs mode but obviously it would be preferable to have a more authoritative source. And yes, we could simply rename all identifiers to start, say, with tla_, but that's not terribly readable.
Thanks,
Stephan
Email Gateway (Jan 16 2021 at 13:03):From: Makarius <makarius@sketis.net>
The short answer: simply use double quotes around your generated identifiers,
e.g. like this for Isabelle BibTeX support:
https://isabelle.sketis.net/repos/isabelle-release/file/Isabelle2021-RC2/src/Pure/Thy/bibtex.scala#l29
Thus you don't need to care about the keywords.
Alternative long answer:
The ancient static elisp tables are now Isabelle/Scala operations to produce
proper data structures from the theory and session source tree.
The included Isabelle/Scala tool works with Isabelle2021-RC2: it inspects the
overall source dependencies to access Outer_Syntax keywords. You can put the
.scala file e.g. in a directory $ISABELLE_HOME_USER/Tools and add this to
$ISABELLE_HOME_USER/etc/settings:
ISABELLE_TOOLS="$ISABELLE_TOOLS:$ISABELLE_HOME_USER/Tools"
Now the following example invocations work:
isabelle outer_keywords Pure
isabelle outer_keywords HOL-Library.Multiset
isabelle outer_keywords -d '$AFP' Akra_Bazzi.Master_Theorem
If you actually need inner keywords for the term language: it is possible to
inspect the global theory syntax in Isabelle/ML and retrieve keywords in a
similar manner. (This won't cover local theory syntax, of course.)
Makarius
outer_keywords.scala
Last updated: Jan 04 2025 at 20:18 UTC