# HG changeset patch
# User wenzelm
# Date 1452883837 -3600
# Node ID 155d30f721dd7e465b9640b550b7f44ecf8b1970
# Parent  3764797dd6fcece56d8dd1301cc7bad9a2b8246d
misc updates and tuning;
more on "Output" versus "Proof state";

diff -r 3764797dd6fc -r 155d30f721dd src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Fri Jan 15 17:30:04 2016 +0100
+++ b/src/Doc/JEdit/JEdit.thy	Fri Jan 15 19:50:37 2016 +0100
@@ -369,7 +369,7 @@
 
     \<^item> \<^emph>\<open>Global Options / Text Area / Text font\<close>: the main text area font,
     which is also used as reference point for various derived font sizes,
-    e.g.\ the Output (\secref{sec:output}) and State
+    e.g.\ the \<^emph>\<open>Output\<close> (\secref{sec:output}) and \<^emph>\<open>State\<close>
     (\secref{sec:state-output}) panels.
 
     \<^item> \<^emph>\<open>Global Options / Gutter / Gutter font\<close>: the font for the gutter area
@@ -745,10 +745,13 @@
 
   \<^medskip>
   \begin{tabular}{lll}
-  \<^bold>\<open>mode\<close> & \<^bold>\<open>file extension\<close> & \<^bold>\<open>content\<close> \\\hline
-  \<^verbatim>\<open>isabelle\<close> & \<^verbatim>\<open>.thy\<close> & theory source \\
-  \<^verbatim>\<open>isabelle-ml\<close> & \<^verbatim>\<open>.ML\<close> & Isabelle/ML source \\
-  \<^verbatim>\<open>sml\<close> & \<^verbatim>\<open>.sml\<close> or \<^verbatim>\<open>.sig\<close> & Standard ML source \\
+  \<^bold>\<open>mode\<close> & \<^bold>\<open>file name\<close> & \<^bold>\<open>content\<close> \\\hline
+  \<^verbatim>\<open>isabelle\<close> & \<^verbatim>\<open>*.thy\<close> & theory source \\
+  \<^verbatim>\<open>isabelle-ml\<close> & \<^verbatim>\<open>*.ML\<close> & Isabelle/ML source \\
+  \<^verbatim>\<open>sml\<close> & \<^verbatim>\<open>*.sml\<close> or \<^verbatim>\<open>*.sig\<close> & Standard ML source \\
+  \<^verbatim>\<open>isabelle-root\<close> & \<^verbatim>\<open>ROOT\<close> & session root \\
+  \<^verbatim>\<open>isabelle-options\<close> & & Isabelle options \\
+  \<^verbatim>\<open>isabelle-news\<close> & & Isabelle NEWS \\
   \end{tabular}
   \<^medskip>
 
@@ -785,8 +788,8 @@
   \begin{center}
   \includegraphics[scale=0.333]{theories}
   \end{center}
-  \caption{Theories panel with an overview of the document-model, and some
-  jEdit text areas as editable view on some of the document nodes}
+  \caption{Theories panel with an overview of the document-model, and jEdit
+  text areas as editable views on some of the document nodes}
   \label{fig:theories}
   \end{figure}
 
@@ -811,22 +814,21 @@
   indicate theory nodes as \<^emph>\<open>required\<close> for continuous checking: this means
   such nodes and all their imports are always processed independently of the
   visibility status (if continuous checking is enabled). Big theory libraries
-  that are marked as required can have significant impact on performance,
-  though.
+  that are marked as required can have significant impact on performance!
 
   \<^medskip>
   Formal markup of checked theory content is turned into GUI rendering, based
-  on a standard repertoire known from IDEs for programming languages: colors,
-  icons, highlighting, squiggly underlines, tooltips, hyperlinks etc. For
-  outer syntax of Isabelle/Isar there is some traditional syntax-highlighting
-  via static keywords and tokenization within the editor; this buffer syntax
-  is determined from theory imports. In contrast, the painting of inner syntax
-  (term language etc.)\ uses semantic information that is reported dynamically
-  from the logical context. 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>\<open>sendback\<close>
-  markup by automated provers or disprovers in the background).
-\<close>
+  on a standard repertoire known from mainstream IDEs for programming
+  languages: colors, icons, highlighting, squiggly underlines, tooltips,
+  hyperlinks etc. For outer syntax of Isabelle/Isar there is some traditional
+  syntax-highlighting via static keywords and tokenization within the editor;
+  this buffer syntax is determined from theory imports. In contrast, the
+  painting of inner syntax (term language etc.)\ uses semantic information
+  that is reported dynamically from the logical context. 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>\<open>sendback\<close> markup by automated provers or
+  disprovers in the background). \<close>
 
 
 subsection \<open>Auxiliary files \label{sec:aux-files}\<close>
@@ -873,8 +875,8 @@
   active (see also \secref{sec:output}).
 
   Warnings, errors, and other useful markup is attached directly to the
-  positions in the auxiliary file buffer, in the manner of other well-known
-  IDEs. By using the load command @{command SML_file} as explained in @{file
+  positions in the auxiliary file buffer, in the manner of standard IDEs. By
+  using the load command @{command SML_file} as explained in @{file
   "$ISABELLE_HOME/src/Tools/SML/Examples.thy"}, Isabelle/jEdit may be used as
   fully-featured IDE for Standard ML, independently of theory or proof
   development: the required theory merely serves as some kind of project file
@@ -892,70 +894,88 @@
   \figref{fig:output}). In the latter case, the corresponding messages are
   shown by hovering with the mouse over the highlighted text --- although in
   many situations the user should already get some clue by looking at the
-  position of the text highlighting, without the text itself.
+  position of the text highlighting, without seeing the message body itself.
 
   \begin{figure}[!htb]
   \begin{center}
   \includegraphics[scale=0.333]{output}
   \end{center}
-  \caption{Multiple views on prover output: gutter area with icon,
-    text area with popup, overview area, Theories panel, Output panel}
+  \caption{Multiple views on prover output: gutter with icon, text area with
+  popup, text overview column, \<^emph>\<open>Theories\<close> panel, \<^emph>\<open>Output\<close> panel}
   \label{fig:output}
   \end{figure}
 
-  The ``gutter area'' on the left-hand-side of the text area uses icons to
-  provide a summary of the messages within the adjacent line of text. Message
+  The ``gutter'' on the left-hand-side of the text area uses icons to
+  provide a summary of the messages within the adjacent text line. Message
   priorities are used to prefer errors over warnings, warnings over
-  information messages, but plain output is ignored.
+  information messages; other output is ignored.
 
-  The ``overview area'' on the right-hand-side of the text area uses similar
-  information to paint small rectangles for the overall status of the whole
-  text buffer. The graphics is scaled to fit the logical buffer length into
-  the given window height. Mouse clicks on the overview area position the
-  cursor approximately to the corresponding line of text in the buffer.
+  The ``text overview column'' on the right-hand-side of the text area uses
+  similar information to paint small rectangles for the overall status of the
+  whole text buffer. The graphics is scaled to fit the logical buffer length
+  into the given window height. Mouse clicks on the overview area move the
+  cursor approximately to the corresponding text line in the buffer.
 
-  Another course-grained overview is provided by the \<^emph>\<open>Theories\<close> panel, but
-  without direct correspondence to text positions. A double-click on one of
-  the theory entries with their status overview opens the corresponding text
-  buffer, without changing the cursor position.
+  The \<^emph>\<open>Theories\<close> panel provides another course-grained overview, but without
+  direct correspondence to text positions. The coloured rectangles represent
+  the amount of messages of a certain kind (warnings, errors, etc.) and the
+  execution status of commands. A double-click on one of the theory entries
+  with their status overview opens the corresponding text buffer, without
+  moving the cursor to a specific point.
 
   \<^medskip>
-  In addition, the \<^emph>\<open>Output\<close> panel displays prover messages that correspond to
-  a given command, within a separate window.
-
-  The cursor position in the presently active text area determines the prover
-  command whose cumulative message output is appended and shown in that window
-  (in canonical order according to the internal execution of the command).
-  There are also control elements to modify the update policy of the output
-  wrt.\ continued editor movements. This is particularly useful with several
-  independent instances of the \<^emph>\<open>Output\<close> panel, which the Dockable Window
-  Manager of jEdit can handle conveniently.
+  The \<^emph>\<open>Output\<close> panel displays prover messages that correspond to a given
+  command, within a separate window. The cursor position in the presently
+  active text area determines the prover command whose cumulative message
+  output is appended and shown in that window (in canonical order according to
+  the internal execution of the command). There are also control elements to
+  modify the update policy of the output wrt.\ continued editor movements:
+  \<^emph>\<open>Auto update\<close> and \<^emph>\<open>Update\<close>. This is particularly useful for multiple
+  instances of the \<^emph>\<open>Output\<close> panel to look at different situations.
+  Alternatively, the panel can be turned into a passive \<^emph>\<open>Info\<close> window via the
+  \<^emph>\<open>Detach\<close> menu item.
 
-  Former users of the old TTY interaction model (e.g.\ Proof~General) might
-  find a separate window for prover messages familiar, but it is important to
-  understand that the main Prover IDE feedback happens elsewhere. It is
-  possible to do meaningful proof editing within the primary text area and its
-  markup, while using secondary output windows only rarely.
+  Proof state is handled separately (\secref{sec:state-output}), but it is
+  also possible to tick the corresponding checkbox to append it to regular
+  output (\figref{fig:output-including-state}). This is a globally persistent
+  option: it affects all open panels and future editor sessions.
 
-  The main purpose of the output window is to ``debug'' unclear situations by
-  inspecting internal state of the prover.\<^footnote>\<open>In that sense, unstructured tactic
-  scripts depend on continuous debugging with internal state inspection.\<close>
-  Consequently, some special messages for \<^emph>\<open>tracing\<close> or \<^emph>\<open>proof state\<close> only
-  appear here, and are not attached to the original source.
+  \begin{figure}[!htb]
+  \begin{center}
+  \includegraphics[scale=0.333]{output-including-state}
+  \end{center}
+  \caption{Proof state display within the regular output panel}
+  \label{fig:output-including-state}
+  \end{figure}
 
   \<^medskip>
-  In any case, prover messages also contain markup that may be explored
-  recursively via tooltips or hyperlinks (see
+  Following the IDE principle, regular messages are attached to the original
+  source in the proper place and may be inspected on demand via popups. This
+  excludes messages that are somehow internal to the machinery of proof
+  checking, notably \<^emph>\<open>proof state\<close> and \<^emph>\<open>tracing\<close>.
+
+  In any case, the same display technology is used for small popups and big
+  output windows. The formal text contains markup that may be explored
+  recursively via further popups and hyperlinks (see
   \secref{sec:tooltips-hyperlinks}), or clicked directly to initiate certain
   actions (see \secref{sec:auto-tools} and \secref{sec:sledgehammer}).
 \<close>
 
 
-section \<open>Proof state output \label{sec:state-output}\<close>
+section \<open>Proof state \label{sec:state-output}\<close>
 
 text \<open>
-  FIXME
-  \figref{fig:output-and-state} versus \figref{fig:output-including-state}
+  The main purpose of the Prover IDE is to help the user editing proof
+  documents, with ongoing formal checking by the prover in the background.
+  This can be done to some extent in the main text area alone, especially for
+  well-structured Isar proofs.
+
+  Nonetheless, internal proof state needs to be inspected in many situations
+  of exploration and ``debugging''. The \<^emph>\<open>State\<close> panel shows exclusively such
+  proof state messages without further distraction, while all other messages
+  are displayed in \<^emph>\<open>Output\<close> (\secref{sec:output}).
+  \Figref{fig:output-and-state} shows a typical GUI layout where both panels
+  are open.
 
   \begin{figure}[!htb]
   \begin{center}
@@ -965,15 +985,34 @@
   \label{fig:output-and-state}
   \end{figure}
 
-  \begin{figure}[!htb]
-  \begin{center}
-  \includegraphics[scale=0.333]{output-including-state}
-  \end{center}
-  \caption{Proof state display within the regular output panel}
-  \label{fig:output-including-state}
-  \end{figure}
+  Another typical arrangement has more than one \<^emph>\<open>State\<close> panel open (as
+  floating windows), with \<^emph>\<open>Auto update\<close> disabled to look at an old situation
+  while the proof text in the vicinity is changed. The \<^emph>\<open>Update\<close> button
+  triggers an explicit one-shot update; this operation is also available via
+  the action @{action "isabelle.update-state"} (keyboard shortcut \<^verbatim>\<open>S+ENTER\<close>).
+
+  On small screens, it is occasionally useful to have all messages
+  concatenated in the regular \<^emph>\<open>Output\<close> panel, e.g.\ see
+  \figref{fig:output-including-state}.
+
+  \<^medskip>
+  The mechanics of \<^emph>\<open>Output\<close> versus \<^emph>\<open>State\<close> are slightly different:
+
+    \<^item> \<^emph>\<open>Output\<close> shows information that is continuously produced and already
+    present when the GUI wants to show it. This is implicitly controlled by
+    the visible perspective on the text.
+
+    \<^item> \<^emph>\<open>State\<close> initiates a real-time query on demand, with a full round trip
+    including a fresh print operation on the prover side. This is controlled
+    explicitly when the cursor is moved to the next command (\<^emph>\<open>Auto update\<close>)
+    or the \<^emph>\<open>Update\<close> operation is triggered.
+
+  This can make a difference in GUI responsibility and resource usage within
+  the prover process. Applications with very big proof states that are only
+  inspected in isolation work better with the \<^emph>\<open>State\<close> panel.
 \<close>
 
+
 section \<open>Query \label{sec:query}\<close>
 
 text \<open>