Re: [isabelle] Initialisation of session and nodes: What's changed?
On Thu, 31 Jan 2013, Avi Knoll wrote:
I have been writing a tool that interfaces with the Isabelle/Scala API, and
have previously (with Isabelle 2012) been using the example at
to load theories and run the prover, so that I can collect output and process
theory semantic information as needed.
As the instance method Session.edit_node no longer exists, may I ask what the
current method for loading nodes and running the prover is, please?
I am answering this on isabelle-users, because you merely want to know how
to use public Isabelle/Scala programming interfaces of in a public release
(Isabelle2013), and not argue about the ongoing development process
between the releases.
BTW, this is a continuation of the
Back to your question. https://bitbucket.org/pide/pide_examples version
212919b16b3a is now updated to Isabelle2013. It was interesting to see
myself, how certain functions to manage Isabelle sessions have evolved
Session.update is now the main operation to feed edits into the prover,
but there were more changes concerning Thy_Load etc.
What is notable is the isabelle.Build module of Isabelle/Scala to manage
Isabelle sessions "offline", without starting a prover process yet; e.g.
you can get hold of the all-important outer syntax that is required for
editing operations. The internal protocols for this have changed
substantially, but they were never public in the first place.
The "isabelle build" shell wrapper is merely some old-fashioned bash
access to the rich functionality of isabelle.Build. Both are equal in
being user-space tools to work with Isabelle systematically -- it does not
make sense to say bash is user-space and Scala not. (Bash is actually
quite far removed for Isabelle users on Windows, so it will gradually be
de-emphasized in favour of Isabelle/Scala, also with some GUI wrappers.)
This archive was generated by a fusion of
Pipermail (Mailman edition) and