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
slowness).
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.)
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
