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



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

The Isabelle code looks correct (and indeed, it builds fine).

As for the Scala code, there are two problems, but they can be easily fixed:

-  val Iterator = implicitly[Int, XML.tree]("iterator")
+  val Iterator = implicitly[math.BigInt, XML.Tree]("iterator")

Conceptually, an ML 'int' can have an arbitrary size, but a JVM 'Int' is
only 32 bits. Hence, it is modelled as a BigInt. Additionally, the
'XML.Tree' is uppercase.

I also guess that you're not going to need the 'ITERATOR' declaration in
the Java API, unless you want to use the Java API.

Cheers
Lars




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