[isabelle-dev] Cartouches in Isabelle/ML

[Makarius]

In ~~/src/HOL/ex/Cartouches_Examples.thy version f4b6e2626cf8 there are 
some additional experiments with cartouches in Isabelle/ML. The main point 
is this:

ML ‹
   val s: Input.source = ‹abc›;
›

i.e. there is notation for formal input source in ML, which includes 
position information that is relevant for PIDE markup.

The subsequent examples in the file play with that a little.


At the moment this is just an exploration of what is possible.  Further 
practical consequences are still to be seen.  For example, one could 
change Syntax.read_term and *all* derivatives of it (definitional packages 
etc.) to use type Input.source instead of string, such that funny YXML 
markup in those strings may be discontinued.  That would be a rather 
drastic change of ML signatures, though.


 	Makarius

----------------------------------------------------------------------------
                   http://stop-ttip.org  1,127,799 people so far
----------------------------------------------------------------------------