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