# 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} *}