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

[Makarius]

*** Prover IDE -- Isabelle/Scala/jEdit ***

* IDE support for the Isabelle/Pure bootstrap process, with the
following independent stages:

   src/Pure/ROOT0.ML
   src/Pure/ROOT.ML
   src/Pure/Pure.thy
   src/Pure/ML_Bootstrap.thy

The ML ROOT files act like quasi-theories in the context of theory
ML_Bootstrap: this allows continuous checking of all loaded ML files.
The theory files are presented with a modified header to import Pure
from the running Isabelle instance. Results from changed versions of
each stage are *not* propagated to the next stage, and isolated from the
actual Isabelle/Pure that runs the IDE itself. The sequential
dependencies of the above files are only relevant for batch build.


This is an update according to Isabelle/785a59235a15.

In practice, it means that regular users who hover-click on some Pure Isar 
command like 'definition', 'theorem' etc. will end up in Pure.thy with IDE 
markup on the ML wrappers for these commands. Hover-clicking there refers 
to ML files of Pure, but without IDE support by default. Opening ROOT.ML 
will make this active as well, but it requires more crunching of the 
compiler.


In the next round, one could try to include the Poly/ML basis library into 
the IDE bootstrap process, but I have presently no clue how that is done.


 	Makarius