Re: [isabelle] libisabelle: embedding into application



Hi,

> Since ancient Isabelle versions our back-end heavily uses
> Thy_Info.get_theory, which only works if used within a proper session [1].
> 
> So our question: Would it be possible to extend Protocol.thy with a
> "operation_setup use_session" ?

when the prover is loaded with a particular session (in your case, it's
probably the session defined in 'libisabelle'), you can't change it
later. You can only load further theories.

However, you can easily start up the prover with a combined session of
all the things you need. You need to make sure that your modified
'Protocol.thy' is included in your 'ROOT' file (either via a theory
import or by listing it explicitly) and then use:

  JSystem sys = JSystem.instance(new File("/path/to/isac"), "Isac");

Cheers
Lars




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