--- 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