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





On 2015-04-21 16:38, Walther Neuper wrote:
Hi Lars,

after merging your last commit Apr.12 2015 from

    https://github.com/larsrh/libisabelle

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 Hello_PIDE.java 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 ---

[error] /home/wneuper/proto4/libisabelle/libisabelle/src/main/scala/Operation.scala:14: type tree is not a member of object isabelle.XML
[error]   val Iterator = implicitly[Int, XML.tree]("iterator")
[error]                                      ^

i.e.: what type declaration is required here ?

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

Walther

[1] https://github.com/wneuper/libisabelle


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:

   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.