*** General ***
* Old-style inner comments (* ... *) within the term language are no
longer supported (legacy feature in Isabelle2018).
This refers to Isabelle/6e9df530b441.
There were a few remaining uses in AFP. Notable changes are
AFP/58b893c52562 and AFP/bf2659bf0a46, where I had to edit sources
generated by LEM (!). I don't know how LEM is maintained: it needs to
produce different inner comments next time, and can actually use
\<comment> CARTOUCHE notation uniformly for inner and outer comments --
also note that this needs to be LaTeX-conformant, e.g. by another nested
cartouche or \<^verbatim>CARTOUCHE.
Now that (* ... *) is no longer part of the term language, Tobias can
finish the infix syntax update project, to get rid of the slightly odd
extra spaces for infixes with *.
There is also a chance that this will speed up the inner parser and/or
grammar updates, which happen quite often (e.g. for local syntax).
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
