more documentation;
Sun, 08 Jan 2017 19:34:44 +0100
changeset 64842 9c69b495c05d
parent 64841 d53696aed874
child 64843 048aa6ea3d32
more documentation;
--- a/NEWS	Sun Jan 08 19:08:26 2017 +0100
+++ b/NEWS	Sun Jan 08 19:34:44 2017 +0100
@@ -13,6 +13,13 @@
 entry of the specified logic session in the editor, while its parent is
 used for formal checking.
+* 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.
 *** HOL ***
--- a/src/Doc/JEdit/JEdit.thy	Sun Jan 08 19:08:26 2017 +0100
+++ b/src/Doc/JEdit/JEdit.thy	Sun Jan 08 19:34:44 2017 +0100
@@ -850,12 +850,16 @@
-  Certain events to open or update editor buffers cause Isabelle/jEdit to
-  resolve dependencies of theory imports. The system requests to load
-  additional files into editor buffers, in order to be included in the
-  document model for further checking. It is also possible to let the system
-  resolve dependencies automatically, according to the system option
-  @{system_option jedit_auto_load}.
+  Theory imports are resolved automatically by the PIDE document model: all
+  required files are loaded and stored internally, without the need to open
+  corresponding jEdit buffers. Opening or closing editor buffers later on has
+  no impact on the formal document content: it only affects visibility.
+  In contrast, auxiliary files (e.g.\ from \<^verbatim>\<open>ML_file\<close> commands) are \<^emph>\<open>not\<close>
+  resolved within the editor by default, but the prover process takes care of
+  that. This may be changed by enabling the system option @{system_option
+  jedit_auto_resolve}: it ensures that all files are uniformly provided by the
+  editor.
   The visible \<^emph>\<open>perspective\<close> of Isabelle/jEdit is defined by the collective