[isabelle-dev] NEWS: text cartouches

[Makarius]

* Lexical syntax (inner and outer) supports text cartouches with
arbitrary nesting, and without escapes of quotes etc.

This refers to Isabelle/3eb7bcca5b90.


LCF-style provers had funny quotes, backquotes, antiquotes etc. from early 
on, and there were occasional attempts to get rid of them.  Just dropping 
quotes and pretending that there is just one big syntax ends up in a 
melange that is hard to define, and sub-languages tend to fight over 
different kinds of keywords versus identifiers etc.  (Even some Coq 
experts now regret that they had gone that way many years ago.)

Postmodern Isabelle/Isar has accumulated various alternative quotation 
forms with slightly different rules for nesting and escapes:

   {* ... *}
   " ... "
   ` ... `
   '' ... ''

Together with antiquotations this quickly runs into limitations of 
syntactic expression, of what is conceptually no problem: the arbitrary 
nesting of "domain-specific formal languages".

Examples:

lemma "A ⟶ A" by (tactic {* rtac @{thm impI} 1 *})

ML {* @{lemma "A ⟶ A" by (tactic "rtac @{thm impI} 1")} *}

text {* @{ML "@{lemma \"A ⟶ A\" by (tactic \"rtac @{thm impI} 1\")}"} *}
   -- "!?!?!?"


Gladly the ancient Egyptians had a different way to "quote" the royal name 
of the Pharao: http://en.wikipedia.org/wiki/Cartouches

An alternative explanation for the name for this syntactic device is 
http://en.wikipedia.org/wiki/Cartouche_%28design%29


In Isabelle it looks like this: symbols \<open> ... \<close> define the 
boundary of a text range, with arbitrary nesting and no escapes nor 
special rules for the body.  The unicode rendering uses the rarely used 
codepoints ‹ ... › to make this look nice and non-intrusive.  Both the 
Isabelle symbols and unicode glyphs are sufficiently exotic to stay 
outside of usual application languages.

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:

text_cartouche
‹
   @{ML_cartouche
     ‹
       (
         @{term_cartouche ‹STR ""›};
         @{term_cartouche ‹STR "abc"›};
         @{term_cartouche ‹STR "abc" @ STR "xyz"›};
         @{term_cartouche ‹STR "⏎"›};
         @{term_cartouche ‹STR "\001\010\100"›}
       )
     ›
   }
›

Here the inner quotes are Isabelle/HOL string literals!

Isabelle/jEdit already knows about these special parantheses, so the 
ragular jEdit operations to work with "code blocks" can be used, e.g. to 
select or navigate through the nested structure.


For the moment this is just some fresh air to get new ideas.  I don't 
propose any bigger reforms just now.

The only concrete change that is already active is a slightly simplified 
syntax for the @{rail} antiquotation, which avoids escapes of backslashes 
and quotes in the body.  (See examples in $ISABELLE_HOME/src/Doc/IsarRef 
and elsewhere.)


 	Makarius