[isabelle-dev] Cartouches in Isabelle/ML

Makarius makarius at sketis.net
Thu Dec 11 12:04:58 CET 2014

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.


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

More information about the isabelle-dev mailing list