# HG changeset patch
# User wenzelm
# Date 1383493792 -3600
# Node ID 7b127966a1fa7f882450dbb252c132a176c9c599
# Parent  9d19298d36508d83e7b382f86af8cb9c1e6eee8c
tuned;

diff -r 9d19298d3650 -r 7b127966a1fa src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Sun Nov 03 16:37:54 2013 +0100
+++ b/src/Doc/JEdit/JEdit.thy	Sun Nov 03 16:49:52 2013 +0100
@@ -468,9 +468,9 @@
 
   \medskip A black rectangle in the text indicates a hyperlink that
   may be followed by a mouse click (while the @{verbatim CONTROL} or
-  @{verbatim COMMAND} modifier key is still pressed). Presently (2013)
-  there is no systematic way to return to the original location within
-  the editor.
+  @{verbatim COMMAND} modifier key is still pressed). Presently
+  (Isabelle2013-1) there is no systematic way to return to the
+  original location within the editor.
 
   Also note that the link target may be a file that is itself not
   subject to formal document processing of the editor session and thus
@@ -480,6 +480,41 @@
   markup is less detailed. *}
 
 
+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.
+
+  Various Isabelle plugin options control the popup behavior and immediate
+  insertion into buffer.
+
+  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"}.
+
+  \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.
+
+  \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.
+
+  \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.
+*}
+
+
 section {* Isabelle symbols *}
 
 text {* Isabelle sources consist of \emph{symbols} that extend plain
@@ -639,41 +674,6 @@
   @{verbatim "\\"}@{verbatim bold} as for regular symbols.  *}
 
 
-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.
-
-  Various Isabelle plugin options control the popup behavior and immediate
-  insertion into buffer.
-
-  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"}.
-
-  \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.
-
-  \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.
-
-  \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.
-*}
-
-
 section {* Automatically tried tools \label{sec:auto-tools} *}
 
 text {* Continuous document processing works asynchronously in the