# HG changeset patch
# User wenzelm
# Date 1380451480 -7200
# Node ID 1f4d6870b7b22ddb43284fa65cb5edee4cc2a7f7
# Parent  7e6a82c593f49f0d867dca1c06e570a6d2767032
more on text completion;

diff -r 7e6a82c593f4 -r 1f4d6870b7b2 NEWS
--- 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.
diff -r 7e6a82c593f4 -r 1f4d6870b7b2 src/Doc/JEdit/JEdit.thy
--- 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 *}