[isabelle-dev] NEWS: formal comments for inner syntax etc.

[Makarius]

*** 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