Re: [isabelle] libisabelle: embedding on ML-side
I'm slightly confused about the current state of affairs here ... I'll
try my best to answer.
>From a previous mail:
> # 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");
The "File" object specifies the session root directory. Everything in
there will be added to the list of known sessions. Since Isabelle
already knows about its bundled sessions, adding $ISABELLE_HOME again
will naturally lead to duplicate sessions.
I take it that "/usr/local/isabisac" contains the full Isabelle
distribution with added Isac? I was expecting that you would specify
just the subdirectory of the Isac component.
Anyway, maybe using "." as path instead of $ISABELLE_HOME works.
> Why not leave (PS(4))
> JSystem.instance(new File("."), "Protocol");
> as it was originally and import from isabisac this way (PS(2,3))
> theory Protocol
> imports Codec "~~/src/Tools/isac/Frontend/Frontend"
It is a bit odd since you're including a "user-space" theory in a
"system-space" theory, but since all theories in an image are "equal"
regardless of their provenance, but conceptually, I don't see why this
This archive was generated by a fusion of
Pipermail (Mailman edition) and