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



Hi Lars,

now I have a situation, which you can reproduce easily:

   Hello_PIDE:
- JSystem sys = JSystem.instance(new File("/usr/local/isabisac"), "Isac"); + JSystem sys = JSystem.instance(new File("/usr/local/Isabelle2014"), "HOL");

This gives:

libisabelle$ export ISABELLE_HOME=/usr/local/Isabelle2014
libisabelle$ /usr/local/Isabelle2014/bin/isabelle build -D . -bv
   (* !!! session Protocol = (*Pure*) HOL + takes its time *)
libisabelle$ ./sbt full/assembly
   (* ok *)
libisabelle$ java -cp full/target/scala-2.11/libisabelle-full.jar Hello_PIDE
   Hello I'm 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)
   :

Do you have an idea, what is wrong here ?

Walther

PS[2]: Summary of the situation:
# Isabelle2014 without any changes

# The libisabelle-side in the mail applies to ...
https://github.com/wneuper/libisabelle/commit/9e02c862175458867d492f3f0dd0aa7c79bd2d9f
# ... with respective updates:
  * session Protocol = (*Pure*) HOL +
  * Hello_PIDE:
      -   JSystem sys = JSystem.instance(new File("."), "Protocol");
+ JSystem sys = JSystem.instance(new File("/usr/local/Isabelle2014"), "HOL");





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