--- a/NEWS Sun Sep 29 12:21:11 2013 +0200
+++ b/NEWS Sun Sep 29 12:44:40 2013 +0200
@@ -77,36 +77,8 @@
such command executions while editing.
* Improved completion mechanism, which is now managed by the
-Isabelle/jEdit plugin instead of SideKick.
-
- - Various Isabelle plugin options to control popup behavior and
- immediate insertion into buffer.
-
- - Light-weight popup, which avoids explicit window (more reactive
- and more robust). Interpreted key events include TAB, ESCAPE, UP,
- DOWN, PAGE_UP, PAGE_DOWN. All other key events are passed to
- the jEdit text area.
-
- - Explicit completion via standard jEdit shortcut C+b, which has
- been remapped to action "isabelle.complete" (fall-back on regular
- "complete-word" for non-Isabelle buffers).
-
- - Implicit completion via keyboard input on text area, with popup or
- immediate insertion into buffer.
-
- - Implicit completion of plain words requires at least 3 characters
- (was 2 before).
-
- - Immediate completion ignores plain words; it requires > 1
- characters of symbol abbreviation to complete, otherwise fall-back
- on completion popup.
-
- - Isabelle Symbols are only completed in backslashed forms,
- e.g. \forall or \<forall> that both produce the Isabelle symbol
- \<forall> in its Unicode rendering.
-
- - Refined table of Isabelle symbol abbreviations (see
- $ISABELLE_HOME/etc/symbols).
+Isabelle/jEdit plugin instead of SideKick. Refined table of Isabelle
+symbol abbreviations (see $ISABELLE_HOME/etc/symbols).
* Support for asynchronous print functions, as overlay to existing
document content.
--- a/src/Doc/JEdit/JEdit.thy Sun Sep 29 12:21:11 2013 +0200
+++ b/src/Doc/JEdit/JEdit.thy Sun Sep 29 12:44:40 2013 +0200
@@ -1,3 +1,5 @@
+(*:wrap=hard:maxLineLen=78:*)
+
theory JEdit
imports Base
begin
@@ -175,7 +177,36 @@
section {* Text completion *}
-text {* FIXME *}
+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 "~~/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.
+*}
chapter {* Known problems and workarounds *}