more documentation;
authorwenzelm
Sun Jan 08 19:34:44 2017 +0100 (2017-01-08)
changeset 648429c69b495c05d
parent 64841 d53696aed874
child 64843 048aa6ea3d32
more documentation;
NEWS
src/Doc/JEdit/JEdit.thy
     1.1 --- a/NEWS	Sun Jan 08 19:08:26 2017 +0100
     1.2 +++ b/NEWS	Sun Jan 08 19:34:44 2017 +0100
     1.3 @@ -13,6 +13,13 @@
     1.4  entry of the specified logic session in the editor, while its parent is
     1.5  used for formal checking.
     1.6  
     1.7 +* The PIDE document model maintains file content independently of the
     1.8 +status of jEdit editor buffers. Reloading jEdit buffers no longer causes
     1.9 +changes of formal document content. Theory dependencies are always
    1.10 +resolved internally, without the need for corresponding editor buffers.
    1.11 +The system option "jedit_auto_load" has been discontinued: it is
    1.12 +effectively always enabled.
    1.13 +
    1.14  
    1.15  *** HOL ***
    1.16  
     2.1 --- a/src/Doc/JEdit/JEdit.thy	Sun Jan 08 19:08:26 2017 +0100
     2.2 +++ b/src/Doc/JEdit/JEdit.thy	Sun Jan 08 19:34:44 2017 +0100
     2.3 @@ -850,12 +850,16 @@
     2.4    \label{fig:theories}
     2.5    \end{figure}
     2.6  
     2.7 -  Certain events to open or update editor buffers cause Isabelle/jEdit to
     2.8 -  resolve dependencies of theory imports. The system requests to load
     2.9 -  additional files into editor buffers, in order to be included in the
    2.10 -  document model for further checking. It is also possible to let the system
    2.11 -  resolve dependencies automatically, according to the system option
    2.12 -  @{system_option jedit_auto_load}.
    2.13 +  Theory imports are resolved automatically by the PIDE document model: all
    2.14 +  required files are loaded and stored internally, without the need to open
    2.15 +  corresponding jEdit buffers. Opening or closing editor buffers later on has
    2.16 +  no impact on the formal document content: it only affects visibility.
    2.17 +
    2.18 +  In contrast, auxiliary files (e.g.\ from \<^verbatim>\<open>ML_file\<close> commands) are \<^emph>\<open>not\<close>
    2.19 +  resolved within the editor by default, but the prover process takes care of
    2.20 +  that. This may be changed by enabling the system option @{system_option
    2.21 +  jedit_auto_resolve}: it ensures that all files are uniformly provided by the
    2.22 +  editor.
    2.23  
    2.24    \<^medskip>
    2.25    The visible \<^emph>\<open>perspective\<close> of Isabelle/jEdit is defined by the collective