*** Document preparation ***
* Embedded languages such as inner syntax and ML may contain formal
comments of the form "\<comment> \<open>text\<close>". As in marginal
comments of outer
syntax, antiquotations are interpreted wrt. the presentation context of
the enclosing command.
This refers to Isabelle/e9bee1ddfe19. It means that inner and outer
syntax comments work uniformly (with the same context), and arbitrary
embedded languages benefit as well (e.g. Isabelle/ML or the "rail"
language).
Also note that there is fancy notation by the IsabelleText font:
"\<comment> \<open>text\<close>" looks like "― ‹text›" in the Prover IDE.
Moreover note that the existing tool "isabelle update_cartouches -c -t"
updates outer syntax to that fancy form (and more).
Isabelle/7360fe6bb423 is an example for a change to "prefer formal
comments": this requires delicate work by hand, because the intended
meaning of a comment can vary:
(1) comment as plain text (with regular typesetting in the document)
(2) comment containing formal text, e.g. @{term} or @{cartouche}
(3) old/unwanted source text that is actually "commented-out"
I am in the process the update cases (1) and (2) in all of Isabelle +
AFP, but case (3) is still untouched. The latter might require a
different formal notation, e.g. \<^blank>\<open>text\<close>.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
