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

Makarius makarius at sketis.net
Sat Apr 9 21:55:30 CEST 2016

On Thu, 7 Apr 2016, Makarius wrote:

> *** Prover IDE -- Isabelle/Scala/jEdit ***
> * IDE support for the Isabelle/Pure bootstrap process.

After further refinements (e.g. see current Isabelle/79f41fbdf74a), the 
Pure IDE bootstrap works even more smoothly. In particular it can be 
combined with this earlier NEWS item:

*** ML ***

* The ML function "ML" provides easy access to run-time compilation.
This is particularly useful for conditional compilation, without
requiring separate files.

An example for such conditional compilation is src/Pure/System/bash.ML, 
with a Windows and POSIX version in the same file. The PIDE markup works
here as expected -- on the one version that is actually taken.


More information about the isabelle-dev mailing list