[isabelle-dev] NEWS: cartouches in "text" and "altstring"

[Makarius]

* The outer syntax categories "text" (for formal comments and document
markup commands) and "altstring" (for literal fact references) allow
cartouches as well, in addition to the traditional mix of quotations.


This refers to Isabelle/7e0178c84994 and Isabelle/90f17a04567d, which also 
contain some examples.

The verbatim {* ... *} token syntax was introduced a long time ago to 
approximate a text delimiter that does not interfere with the other 
quotations.  The cartouche variant manages that better, with the 
possibilities we have today.

The altstring `...` token syntax with ASCII back-quotes was already 
rendered with single guillemets in latex before, and the Isabelle/jEdit 
symbol abrreviation re-uses ` to produce the same in the editor, so it is 
natural to make this identification official.  It also helps to avoid a 
conflict with occasional backquotes in the term language.


Right now there is no ambition to "standardize" existing Isabelle sources. 
At some point it could be done systematically with some Isabelle/Scala 
tool that has access to the semantic markup of the document.


Concerning the general potential for user confusion about nesting 
different kinds of delimited tokens, see also 
http://stackoverflow.com/questions/22699529/double-quotes-inside-inner-syntax-comment

In such situations I am tempted to point out the "obvious" definitions of 
these syntax categories somewhere, but that is only in the ML and Scala 
sources, not even in the manuals.


 	Makarius