[isabelle-dev] NEWS: embedded YXML syntax

[Makarius]

On Mon, 11 Jul 2011, Alexander Krauss wrote:

> Do you have an example / intended use?

The following is a bit silly, but it demenstrates several layers that can 
be involved here:

ML {*
   val lemma =
     Term_XML.Encode.term #>
     YXML.string_of_body #>
     translate_string (fn c => if ord c < 10 then "\\00" ^ string_of_int (ord c) else c) #>
     quote #> prefix "lemma " #>
     Markup.markup Markup.sendback #> writeln
*}

ML {* lemma @{prop "x == x"} *}

Now you can click on the gibberish in the Output window to get the ML 
proposition pasted into the document as formal goal.


The YXML inner syntax bypass allows to reconstruct programmatic inferfaces 
to packages where people have "forgotten" to provide on in ML.  It also 
facilitates the same from the Scala side, without defining auxiliary Isar 
commands first.  It works uniformly for the usual logical categories: 
sort, typ, term, prop.  (Some user from ETH Zürich has reminded me that 
something like this was in the pipeline for a long time.)


The Term_XML (and XML_Data) structures/objects are also nice examples of 
higher-order abstract non-sense.  E.g. see 
http://isabelle.in.tum.de/repos/isabelle/file/52310132063b/src/Pure/term_xml.ML#l41

Of course, Haskell could do better here with type classes for 
(de)serialization.


 	Makarius