Email Gateway (Aug 19 2022 at 10:26): Email Gateway (Aug 19 2022 at 10:26):From: Makarius <makarius@sketis.net>
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
thread
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2012-February/msg00067.html
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
since Isabelle2012.
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.)
Makarius
Last updated: Apr 25 2024 at 08:20 UTC