Re: [isabelle] PIDE by example



> but throw exceptions as soon as I try to return XML (test_2 and
> Iterator, the latter not reached):

The reason why that fails is that by default, the 'sendCommand' function
tries to parse Isabelle's response as string. If you want the raw XML
block back, use 'sendCommandXML', which converts neither input nor output.

I'm not sure how convenient it would be to produce XML trees in Java. In
Scala, it would look like this:

  XML.Encode.int(222)

(This is completely symmetric to 'XML.Decode.int' in Isabelle/ML, which
you're already using.)

Shot in the dark for Java:

  isabelle.XML$.Encode$.int.apply(222);

I may need to add some convenience functions to make that more visually
pleasing.

By the way, there should be no need to use 'XML.parse' in Isabelle/ML.
Instead, you can construct your response like this:

  XML.Elem (("CALCTREE", []),
    [XML.Elem (("CALCID", []), [XML.Text "foo"])])

Cheers
Lars




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.