# HG changeset patch
# User wenzelm
# Date 1402488064 -7200
# Node ID 88d7e3eca84b04679a190b42f8a93dbd637e85ea
# Parent  f7e75bb411b42243d5ee98bfb9b0d20a939e3a11
more on "Document model";

diff -r f7e75bb411b4 -r 88d7e3eca84b src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Mon Jun 09 20:44:13 2014 +0200
+++ b/src/Doc/JEdit/JEdit.thy	Wed Jun 11 14:01:04 2014 +0200
@@ -632,37 +632,85 @@
 
 chapter {* Prover IDE functionality *}
 
-section {* Text buffers and theories \label{sec:buffers-theories} *}
+section {* Document model *}
+
+text {*
+  The document model is central to the PIDE architecture: the editor and the
+  prover have a common notion of structured source text with markup, which is
+  produced by formal processing. The editor is responsible for edits of
+  document source, as produced by the user. The prover is responsible for
+  reports of document markup, as produced by its processing in the background.
+
+  Isabelle/jEdit handles classic editor events of jEdit, in order to connect
+  the physical world of the GUI (with its singleton state) to the mathematical
+  world of multiple document versions (with timeless and stateless updates).
+*}
+
 
-text {* As regular text editor, jEdit maintains a collection of open
-  \emph{text buffers} to store source files; each buffer may be
-  associated with any number of visible \emph{text areas}.  Buffers
-  are subject to an \emph{edit mode} that is determined from the file
-  type.  Files with extension \texttt{.thy} are assigned to the mode
-  \emph{isabelle} and treated specifically.
+subsection {* Editor buffers and document nodes *}
+
+text {*
+  As a regular text editor, jEdit maintains a collection of \emph{buffers} to
+  store text files; each buffer may be associated with any number of visible
+  \emph{text areas}. Buffers are subject to an \emph{edit mode} that is
+  determined from the file name extension. The following modes are treated
+  specifically in Isabelle/jEdit:
+
+  \medskip
+  \begin{tabular}{lll}
+  \textbf{mode} & \textbf{file extension} & \textbf{content} \\\hline
+  @{verbatim "isabelle"} & @{verbatim ".thy"} & theory source \\
+  @{verbatim "isabelle-ml"} & @{verbatim ".ML"} & Isabelle/ML source \\
+  @{verbatim "sml"} & @{verbatim ".sml"} or @{verbatim ".sig"} & Standard ML source \\
+  \end{tabular}
+  \medskip
 
-  \medskip Isabelle theory files are automatically added to the formal
-  document model of Isabelle/Scala, which maintains a family of versions of
-  all sources for the prover. The \emph{Theories} panel provides an overview
-  of the status of continuous checking of theory sources. Unlike batch
-  sessions of @{tool build} \cite{isabelle-sys}, theory nodes are identified
-  by full path names; this allows to work with multiple (disjoint) Isabelle
-  sessions simultaneously within the same editor session.
+  All jEdit buffers are automatically added to the PIDE document-model as
+  \emph{document nodes}. The overall document structure is defined by the
+  theory nodes in two dimensions:
+
+  \begin{enumerate}
+
+  \item via \textbf{theory imports} that are specified in the \emph{theory
+  header} using concrete syntax of the @{command theory} command
+  \cite{isabelle-isar-ref};
+
+  \item via \textbf{auxiliary files} that are loaded into a theory by special
+  \emph{load commands}, notably @{command ML_file} and @{command SML_file}
+  \cite{isabelle-isar-ref}.
+
+  \end{enumerate}
 
-  Certain events to open or update buffers with theory files cause
-  Isabelle/jEdit to resolve dependencies of \emph{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
+  In any case, source files are managed by the PIDE infrastructure: the
+  physical file-system only plays a subordinate role. The relevant version of
+  source text is passed directly from the editor to the prover, via internal
+  communication channels.
+*}
+
+
+subsection {* Theories \label{sec:theories} *}
+
+text {*
+  The \emph{Theories} panel (see also \figref{fig:output}) provides an
+  overview of the status of continuous checking of theory nodes within the
+  document model. Unlike batch sessions of @{tool build} \cite{isabelle-sys},
+  theory nodes are identified by full path names; this allows to work with
+  multiple (disjoint) Isabelle sessions simultaneously within the same editor
+  session.
+
+  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 \emph{Plugin Options /
   Isabelle / General / Auto Load}.
 
-  \medskip The open text area views on theory buffers define the
-  visible \emph{perspective} of Isabelle/jEdit.  This is taken as a
-  hint for document processing: the prover ensures that those parts of
-  a theory where the user is looking are checked, while other parts
-  that are presently not required are ignored.  The perspective is
-  changed by opening or closing text area windows, or scrolling within
-  a window.
+  \medskip The visible \emph{perspective} of Isabelle/jEdit is defined by the
+  collective view on theory buffers via open text areas. The perspective is
+  taken as a hint for document processing: the prover ensures that those parts
+  of a theory where the user is looking are checked, while other parts that
+  are presently not required are ignored. The perspective is changed by
+  opening or closing text area windows, or scrolling within a window.
 
   The \emph{Theories} panel provides some further options to influence
   the process of continuous checking: it may be switched off globally
@@ -684,7 +732,15 @@
   Thus the prover can provide additional markup to help the user to understand
   the meaning of formal text, and to produce more text with some add-on tools
   (e.g.\ information messages with \emph{sendback} markup by automated provers
-  or disprovers in the background). *}
+  or disprovers in the background).
+
+*}
+
+subsection {* Auxiliary files \label{sec:aux-files} *}
+
+text {*
+  FIXME
+*}
 
 
 section {* Output \label{sec:output} *}