[isabelle-dev] NEWS: text cartouches

[Makarius]

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