On Thu, 23 Jan 2014, Makarius wrote:
* Lexical syntax (inner and outer) supports text cartouches with
arbitrary nesting, and without escapes of quotes etc.
This refers to Isabelle/3eb7bcca5b90.
A playground with an exploration of possibilities is in
$ISABELLE_HOME/src/HOL/ex/Cartouche_Examples.thy e.g. see the "Uniform
nesting of sub-languages" example:
This got probably stuck in the middle of ITP2014 paper writing. Did
anybody take a look at the examples, and start thinking about the range of
possibilities? The carnival season is approaching its peak, but there
might be some serious applications that are relevant right now.
In principle one could do away with the traditional double-quotes for the
inner syntax, although that is probably too intrusive after so many
decades. A less ambitious reform is to allow the "text" category
(presently "..." or {*...*}) to use cartouches as well.
(Any change of outer syntax would require some remaining users of historic
front-ends to make a move. In contrast, anything built on top of
Isabelle/Scala works out of the box.)
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
