[isabelle-dev] NEWS: cartouches

[Makarius]

*** General ***

* Embedded content (e.g. the inner syntax of types, terms, props) may be
delimited uniformly via cartouches. This works better than old-fashioned
quotes when sub-languages are nested.


*** Prover IDE -- Isabelle/Scala/jEdit ***

* Cartouche abbreviations work both for " and ` to accomodate typical
situations where old ASCII notation may be updated.


This refers e.g. to Isabelle/4cf6726eb85e, which also contains more
unification of "embedded" language tokens: type, term, prop, text. Thus
the complexity of Isabelle language nesting is reduced, thanks to more
uniform notation.


When demonstrating Isabelle occasionally to people who have never seen
it before, there is often a spontaneous puzzlement about ASCII quotes
around inner syntax. With cartouches that surprise might be avoided,
since it is not associated with already known syntax.

Still missing: a tool for systematic replacement of such semantic
cartouches. Purely syntactic ones are already handled by "isabelle
update_cartouches".


	Makarius