[isabelle-dev] NEWS: PIDE document maintains file content internally

Makarius makarius at sketis.net
Sun Jan 8 20:02:11 CET 2017

*** Prover IDE -- Isabelle/Scala/jEdit ***

* The PIDE document model maintains file content independently of the
status of jEdit editor buffers. Reloading jEdit buffers no longer causes
changes of formal document content. Theory dependencies are always
resolved internally, without the need for corresponding editor buffers.
The system option "jedit_auto_load" has been discontinued: it is
effectively always enabled.

This refers to Isabelle/9c69b495c05d. It is a substantial reform of PIDE
file management to make things more scalable. A few more consequences of
it are still in the pipeline: the ultimate goal (since 2013) is to load
all of AFP into one big PIDE session!

Moreover the accidental meaning of "Reload" and "Reload All" to restart
formal processing has disappeared. I occasionally used that for testing
purposes -- now that needs to be done by actual edits.


More information about the isabelle-dev mailing list