Re: [isabelle] libisabelle: embedding on ML-side




now I have a situation, which can easily be reproduced:

even more easily reproduced:

$ git clone https://github.com/larsrh/libisabelle.git xxxxx

# edit xxxxx/examples/src/main/java/Hello_PIDE.java
     -  JSystem sys = JSystem.instance(new File("."), "Protocol");
+ JSystem sys = JSystem.instance(new File("/usr/local/Isabelle2014"), "HOL");

xxxxx$ export ISABELLE_HOME=/usr/local/Isabelle2014
xxxxx$ /usr/local/Isabelle2014/bin/isabelle build -D . -bv
xxxxx$ ./sbt full/assembly
xxxxx$ java -cp full/target/scala-2.11/libisabelle-full.jar Hello_PIDE
Exception in thread "main" java.lang.RuntimeException: Duplicate session "RAW" (line 3 of "/usr/local/Isabelle2014/src/Pure/ROOT") (line 3 of "/usr/local/Isabelle2014/src/Pure/ROOT")
    at isabelle.Library$ERROR$.apply(library.scala:20)
    :

How can one connect to some session ("HOL" and beyond) on the ML-side?

Hope to have sufficiently pinned down the situation herewith.
Thanks a lot in advance for your support,

Walther




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