Re: [isabelle] libisabelle: Small Scala library to communicate with Isabelle

Hi Lars,

after merging your last commit Apr.12 2015 from

into our repository [1] we checked your and Makarius' suggestions about development environments for Java / Scala / SML and now find it most convenient to compile with your

    $ $ISABELLE_HOME/bin/isabelle build -D . -bv
    $ ./sbt

into *.jar (the former for the ML side and the latter for Java / Scala), edit our files in Eclipse (Protocol.thy and Operation(s).scala for both sides respectively), and execute from the command line (with paths to respective *.jar). This setup seems sufficient for our trials within libisabelle before integration into Isac.

For the above setup we can successfully transfer strings back and forth; however we cannot figure out, how to return an XML.tree ---

--- could you, please, have a look at the last commit e3dd289 <> to [1]: there all compiles without errrors, because the questionable operation is out-commented in all files.



On 2015-02-24 11:56, Lars Hupel wrote:
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:

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

Shot in the dark for Java:


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

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"])])


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