[isabelle-dev] NEWS: embedded YXML syntax

[Makarius]

On Mon, 11 Jul 2011, Makarius wrote:

> On Mon, 11 Jul 2011, Alexander Krauss wrote:
>
>> Do you have an example / intended use?

Here is another example (for Isabelle/c3b6374278fa):

ML {*
   val print_scala =
     Term_XML.Encode.term
     #> YXML.string_of_body
     #> YXML.embed_controls
     #> funpow 3 quote
     #> prefix "val s = "
     #> writeln
*}

ML {* print_scala @{term "%x. x + y + z"} *}

Now the Output window shows some generated Scala text that can be pasted 
manually into the Console/Scala window in jEdit.

(Scala string literals with 3 codes may contain arbitrary control 
characters without escapes.  Display of small black squares instead of 
bold-italic X and Y means the user has an old version of the IsabelleText 
fonts installed on the system.  This needs to be updated from 
Isabelle/lib/fonts, or deleted.  Isabelle/Scala can pick up the font 
automatically, unless the operating system already imposes another version 
onto the JVM by external means.)

Interpreting the generated Scala source defines a String val s.  It can be 
turned into a term in Scala like this:

   import isabelle._
   Term_XML.Decode.term(YXML.parse_body(s))

Now we have a mirror image of the ML term datatype in Scala, see also 
src/Pure/term.scala for the definitions.

This allows to play ping-pong with formal entities between the two 
processes, using the Term_XML and YXML functions on either side.  E.g. 
there could be external tools that happen to run on the JVM and need to be 
connected to the logic, or some IDE components that want to manipulate 
formal entities in some way.  Of course, the main logical operations 
remain on the ML side, where the fully formal context is available (e.g. 
for unification, but also for notation).

Note that producing terms in Scala on the spot is not so easy without 
knowing the context -- hard-wired constant names like in really old 
Isabelle/ML code do not last long.  Formal entities must somehow come from 
the formal environment, potentially based on a mechanism that is similar 
to ML antiquotations.


 	Makarius