[isabelle-dev] NEWS: Auxiliary files

[Makarius]

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