[isabelle-dev] NEWS: IDE support for Isabelle/Pure bootstrap
makarius at sketis.net
Thu Apr 7 17:36:32 CEST 2016
*** Prover IDE -- Isabelle/Scala/jEdit ***
* IDE support for the Isabelle/Pure bootstrap process. The file
src/Pure/ROOT.ML may be opened with Isabelle/jEdit: it acts like a
theory body in the context of theory ML_Bootstrap. This allows
continuous checking of ML files as usual, but the result is isolated
from the actual Isabelle/Pure that runs the IDE itself.
This refers to Isabelle/94535e6dd168, it is the Isabelle/Holodeck that
we've all awaited for years. The structure Thread_Data_Virtual is notable:
it shows how global references can be managed in a value-oriented manner
by the Isabelle framework.
Maybe some other big applications of Poly/ML should be made PIDE-compliant
as well, e.g. HOL4 or even Poly/ML itself.
More information about the isabelle-dev