# HG changeset patch
# User wenzelm
# Date 1483900484 -3600
# Node ID 9c69b495c05d7cf058fb7d96dd352cbaecb8911d
# Parent  d53696aed874cadea6fdf2eb7e8968a75027b13e
more documentation;

diff -r d53696aed874 -r 9c69b495c05d NEWS
--- 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 ***
 
diff -r d53696aed874 -r 9c69b495c05d src/Doc/JEdit/JEdit.thy
--- 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 @@
   \label{fig:theories}
   \end{figure}
 
-  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.
 
   \<^medskip>
   The visible \<^emph>\<open>perspective\<close> of Isabelle/jEdit is defined by the collective