[isabelle-dev] NEWS: IDE support for Isabelle/Pure bootstrap
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