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
shouldn't work.

Cheers
Lars




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