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
----------------------------------------------------------------------------_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
