Re: [isabelle] libisabelle: embedding into application
- To: Walther Neuper <neuper at ist.tugraz.at>
- Subject: Re: [isabelle] libisabelle: embedding into application
- From: Lars Hupel <hupel at in.tum.de>
- Date: Mon, 01 Jun 2015 14:00:14 +0200
- Cc: cl-isabelle-users at lists.cam.ac.uk
- In-reply-to: <556C24A4.firstname.lastname@example.org>
- References: <email@example.com> <556C24A4.firstname.lastname@example.org>
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.7.0
> Since ancient Isabelle versions our back-end heavily uses
> Thy_Info.get_theory, which only works if used within a proper session .
> 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");
This archive was generated by a fusion of
Pipermail (Mailman edition) and