[isabelle-dev] NEWS: Auxiliary files
makarius at sketis.net
Wed Feb 12 16:10:57 CET 2014
On Wed, 20 Nov 2013, Makarius wrote:
> *** Prover IDE -- Isabelle/Scala/jEdit ***
> * Auxiliary files ('ML_file' etc.) are managed by the Prover IDE.
> Open text buffers take precedence over copies within the file-system.
This refers to Isabelle/662e0fd39823 (a changeset before HOL-IMP
The NEWS entry is unchanged, but the implementation is now more complete.
In particular PIDE markup is part of the document model, and shown in the
document view within the editor. This makes a big difference in the
ergonomics of editing Isabelle/ML files.
Note that the theory that loads a file needs to be visited already: this
is not resolved automatically. Moreover switching from implicit loading
to explicit editing of an auxiliary file processes the theory content
again from that point. (To avoid that, the prover would have to be
deprived of file-system access altogether, and everything provided by the
front-end all the time.)
More information about the isabelle-dev