
diff -r 7b127966a1fa -r c5d6cd7ab132 src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Sun Nov 03 16:49:52 2013 +0100
+++ b/src/Doc/JEdit/JEdit.thy	Sun Nov 03 18:12:23 2013 +0100
@@ -482,40 +482,107 @@
 
 section {* Text completion \label{sec:completion} *}
 
-text {*
-  Text completion works via some light-weight GUI popup, which is triggered by
-  keyboard events during the normal editing process in the main jEdit text
-  area and a few additional text fields. The popup interprets special keys:
-  @{verbatim TAB}, @{verbatim ESCAPE}, @{verbatim UP}, @{verbatim DOWN},
-  @{verbatim PAGE_UP}, @{verbatim PAGE_DOWN}. All other key events are passed
-  to the jEdit text area --- this allows to ignore unwanted completions most
-  of the time and continue typing quickly.
+text {* \paragraph{Completion tables} are determined statically from
+  the ``outer syntax'' of the underlying edit mode (for theory files
+  this is the syntax of Isar commands) and specifications of Isabelle
+  symbols (see also \secref{sec:symbols}).
+
+  Symbols are completed in backslashed forms, e.g.\ @{verbatim
+  "\\"}@{verbatim "forall"} or @{verbatim "\<forall>"} that both produce the
+  Isabelle symbol @{text "\<forall>"} in its Unicode rendering.\footnote{The
+  extra backslash avoids overlap with keywords of the buffer syntax,
+  and facilitates to produce Isabelle symbols in arbitrary syntactic
+  contexts.}  Alternatively, symbol abbreviations may be used as
+  specified in @{file "$ISABELLE_HOME/etc/symbols"}.
+
+  \paragraph{Completion popups} are required in situations of
+  ambiguous completion results or where explicit confirmation is
+  demanded before inserting completed text into the buffer.
+
+  The popup is some minimally invasive GUI component over the text
+  area.  It interprets special keys @{verbatim TAB}, @{verbatim
+  ESCAPE}, @{verbatim UP}, @{verbatim DOWN}, @{verbatim PAGE_UP},
+  @{verbatim PAGE_DOWN}, but all other key events are passed to the
+  underlying text area.  This allows to ignore unwanted completions
+  most of the time and continue typing quickly.
 
-  Various Isabelle plugin options control the popup behavior and immediate
-  insertion into buffer.
+  The meaning of special keys is as follows:
+
+  \medskip
+  \begin{tabular}{ll}
+  @{verbatim "TAB"} & select completion \\
+  @{verbatim "ESCAPE"} & dismiss popup \\
+  @{verbatim "UP"} & move up one item \\
+  @{verbatim "DOWN"} & move down one item \\
+  @{verbatim "PAGE_UP"} & move up one page of items \\
+  @{verbatim "PAGE_DOWN"} & move down one page of items \\
+  \end{tabular}
+  \medskip
+
+  Movement within the popup is only active for multiple items.
+  Otherwise the corresponding key event retains its standard meaning
+  within the underlying text area.
+
+  \paragraph{Explicit completion} is triggered by the keyword shortcut
+  @{verbatim "C+b"} for action @{verbatim "isabelle.complete"}.  This
+  overrides the original jEdit action @{verbatim "complete-word"} on
+  that key sequence, but the latter is used as fall-back for
+  non-Isabelle edit modes.  It is also possible to restore the
+  original jEdit keyboard mapping of @{verbatim "complete-word"}.
 
-  Isabelle Symbols are completed in backslashed forms, e.g.\ @{verbatim
-  "\\"}@{verbatim "forall"} or @{verbatim "\<forall>"} that both produce the Isabelle
-  symbol @{text "\<forall>"} in its Unicode rendering. Alternatively, symbol
-  abbreviations may be used as specified in @{file
-  "$ISABELLE_HOME/etc/symbols"}.
+  Replacement text is inserted immediately into the buffer, unless
+  ambiguous results demand an explicit popup.
+
+  \paragraph{Implicit completion} is triggered by regular keyboard
+  input events during of the editing process in the main jEdit text
+  area (and a few additional text fields like the search criterium of
+  the Find panel, see \secref{sec:find}).  Implicit completion depends
+  on on further side-conditions:
+
+  \begin{enumerate}
+
+  \item The system option @{system_option jedit_completion} needs to
+  be enabled (default).
+
+  \item Completion of syntax keywords requires at least 3 characters
+  in the text.
+
+  \item The system option @{system_option jedit_completion} determines
+  an additional delay (0.0 by default), before opening a completion
+  popup.
 
-  \emph{Explicit completion} works via standard jEdit shortcut @{verbatim
-  "C+b"}, which is remapped to action @{verbatim "isabelle.complete"}, with a
-  fall-back on regular @{verbatim "complete-word"} for non-Isabelle buffers.
+  \item The system option @{system_option jedit_completion_immediate}
+  (disabled by default) controls whether replacement text should be
+  inserted immediately without popup, if possible.  This only works
+  for Isabelle symbols (\secref{sec:symbols}).
+
+  \item Completion of symbol abbreviations with only 1 character in
+  the text always enforces and explicit popup, independently of
+  @{system_option jedit_completion_immediate}.
+
+  \end{enumerate}
 
-  \emph{Implicit completion} works via keyboard input on text area, with popup
-  or immediate insertion into buffer. Plain words require at least 3
-  characters to be completed.
+  These completion options may be configured in \emph{Plugin Options /
+  Isabelle / General / Completion}.  The default is quite moderate in
+  showing occasional popups and refraining from immediate insertion.
+  An additional of e.g.\ 0.3 seconds will make it even less ambitious.
 
-  \emph{Immediate completion} means the (unique) replacement text is inserted
-  into the buffer without popup. This mode ignores plain words and requires
-  more than one characters for symbol abbreviations. Otherwise it falls back
-  on completion popup.
+  A more aggressive configuration is @{system_option
+  jedit_completion_delay}~@{verbatim "= 0.0"} and @{system_option
+  jedit_completion_immediate}~@{verbatim "= true"}.  Thus the editing
+  process becomes more dependent on the system guessing correctly what
+  the user had in mind.  It requires some practice and study of the
+  symbol abbreviation tables to be productive in this mode.
+
+  Unintended completions can be reverted by the regular @{verbatim
+  undo} operation of jEdit.  When editing embedded languages such as
+  ML works, it is better to disable either @{system_option
+  jedit_completion} or @{system_option jedit_completion_immediate}
+  temporarily.
 *}
 
 
-section {* Isabelle symbols *}
+section {* Isabelle symbols \label{sec:symbols} *}
 
 text {* Isabelle sources consist of \emph{symbols} that extend plain
   ASCII to allow infinitely many mathematical symbols within the
@@ -810,7 +877,7 @@
   nonetheless, say to remove earlier proof attempts. *}
 
 
-section {* Find theorems *}
+section {* Find theorems \label{sec:find} *}
 
 text {* The \emph{Find} panel (\figref{fig:find}) provides an
   independent view for @{command find_theorems}.  The main text field




