[isabelle-dev] NEWS: IDE support for Isabelle/Pure bootstrap

[Makarius]

*** 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.


 	Makarius