diff -r 7557f9f1d4aa -r 6692c355ebc1 src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Wed Oct 30 18:47:09 2013 +0100
+++ b/src/Doc/JEdit/JEdit.thy	Wed Oct 30 21:23:47 2013 +0100
@@ -296,7 +296,7 @@
 
 chapter {* Prover IDE functionality *}
 
-section {* Text buffers and theories *}
+section {* Text buffers and theories \label{sec:buffers-theories} *}
 
 text {* As regular text editor, jEdit maintains a collection of open
   \emph{text buffers} to store source files; each buffer may be
@@ -356,6 +356,68 @@
 *}
 
 
+section {* Prover output *}
+
+text {* Prover output consists of \emph{markup} and \emph{messages}.
+  Both are directly attached to the corresponding positions in the
+  original source text, and visualized in the text area, e.g.\ as text
+  colours for free and bound variables, or as squiggly underline for
+  warnings, errors etc.  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 text highlighting alone.
+
+  The ``gutter area'' on the left-hand-side of the text area uses
+  icons to provide a summary of the messages within the corresponding
+  line of text.  Message priorities are used to prefer errors over
+  warnings, warnings over information messages etc.  Plain output is
+  ignored here.
+
+  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.
+
+  Another course-grained overview is provided by the \emph{Theories}
+  panel (\secref{sec:buffers-theories}), 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.
+
+  \medskip In addition, the \emph{Output} 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 commands whose cumulative message output is appended an shown
+  in that window (in canonical order according to the processing 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{Output} panel, which the Dockable Window Manager of jEdit can
+  handle conveniently.
+
+  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
+  efficiently while using the secondary window only rarely.
+
+  The main purpose of the output window is to ``debug'' unclear
+  situations by inspecting internal state of the prover.\footnote{In
+  that sense, unstructured tactic scripts depend on continous
+  debugging with internal state inspection.} Consequently, some
+  special messages for \emph{tracing} or \emph{proof state} only
+  appear here, and are not attached to the original source.
+
+  \medskip In any case, prover messages also contain markup that may
+  be explored recursively via tooltips or hyperlinks (see
+  \secref{sec:tooltips-hyperlinks}), or clicked directly to initiate
+  certain actions (e.g.\ see \secref{sec:sledgehammer}).  *}
+
+
 section {* Tooltips and hyperlinks \label{sec:tooltips-hyperlinks} *}
 
 text {* Formally processed text (prover input or output) contains rich
@@ -601,6 +663,27 @@
 *}
 
 
+section {* Automatically tried tools *}
+
+text {*
+  FIXME
+*}
+
+
+section {* Sledgehammer \label{sec:sledgehammer} *}
+
+text {*
+  FIXME
+*}
+
+
+section {* Find theorems *}
+
+text {*
+  FIXME
+*}
+
+
 chapter {* Known problems and workarounds \label{sec:problems} *}
 
 text {*