more on text completion;
authorwenzelm
Sun Sep 29 12:44:40 2013 +0200 (2013-09-29)
changeset 539811f4d6870b7b2
parent 53980 7e6a82c593f4
child 53982 f0ee92285221
more on text completion;
NEWS
src/Doc/JEdit/JEdit.thy
     1.1 --- a/NEWS	Sun Sep 29 12:21:11 2013 +0200
     1.2 +++ b/NEWS	Sun Sep 29 12:44:40 2013 +0200
     1.3 @@ -77,36 +77,8 @@
     1.4  such command executions while editing.
     1.5  
     1.6  * Improved completion mechanism, which is now managed by the
     1.7 -Isabelle/jEdit plugin instead of SideKick.
     1.8 -
     1.9 -  - Various Isabelle plugin options to control popup behavior and
    1.10 -    immediate insertion into buffer.
    1.11 -
    1.12 -  - Light-weight popup, which avoids explicit window (more reactive
    1.13 -    and more robust).  Interpreted key events include TAB, ESCAPE, UP,
    1.14 -    DOWN, PAGE_UP, PAGE_DOWN.  All other key events are passed to
    1.15 -    the jEdit text area.
    1.16 -
    1.17 -  - Explicit completion via standard jEdit shortcut C+b, which has
    1.18 -    been remapped to action "isabelle.complete" (fall-back on regular
    1.19 -    "complete-word" for non-Isabelle buffers).
    1.20 -
    1.21 -  - Implicit completion via keyboard input on text area, with popup or
    1.22 -    immediate insertion into buffer.
    1.23 -
    1.24 -  - Implicit completion of plain words requires at least 3 characters
    1.25 -    (was 2 before).
    1.26 -
    1.27 -  - Immediate completion ignores plain words; it requires > 1
    1.28 -    characters of symbol abbreviation to complete, otherwise fall-back
    1.29 -    on completion popup.
    1.30 -
    1.31 -  - Isabelle Symbols are only completed in backslashed forms,
    1.32 -    e.g. \forall or \<forall> that both produce the Isabelle symbol
    1.33 -    \<forall> in its Unicode rendering.
    1.34 -
    1.35 -  - Refined table of Isabelle symbol abbreviations (see
    1.36 -    $ISABELLE_HOME/etc/symbols).
    1.37 +Isabelle/jEdit plugin instead of SideKick.  Refined table of Isabelle
    1.38 +symbol abbreviations (see $ISABELLE_HOME/etc/symbols).
    1.39  
    1.40  * Support for asynchronous print functions, as overlay to existing
    1.41  document content.
     2.1 --- a/src/Doc/JEdit/JEdit.thy	Sun Sep 29 12:21:11 2013 +0200
     2.2 +++ b/src/Doc/JEdit/JEdit.thy	Sun Sep 29 12:44:40 2013 +0200
     2.3 @@ -1,3 +1,5 @@
     2.4 +(*:wrap=hard:maxLineLen=78:*)
     2.5 +
     2.6  theory JEdit
     2.7  imports Base
     2.8  begin
     2.9 @@ -175,7 +177,36 @@
    2.10  
    2.11  section {* Text completion *}
    2.12  
    2.13 -text {* FIXME *}
    2.14 +text {*
    2.15 +  Text completion works via some light-weight GUI popup, which is triggered by
    2.16 +  keyboard events during the normal editing process in the main jEdit text
    2.17 +  area and a few additional text fields. The popup interprets special keys:
    2.18 +  @{verbatim TAB}, @{verbatim ESCAPE}, @{verbatim UP}, @{verbatim DOWN},
    2.19 +  @{verbatim PAGE_UP}, @{verbatim PAGE_DOWN}. All other key events are passed
    2.20 +  to the jEdit text area --- this allows to ignore unwanted completions most
    2.21 +  of the time and continue typing quickly.
    2.22 +
    2.23 +  Various Isabelle plugin options control the popup behavior and immediate
    2.24 +  insertion into buffer.
    2.25 +
    2.26 +  Isabelle Symbols are completed in backslashed forms, e.g. @{verbatim
    2.27 +  "\\"}@{verbatim "forall"} or @{verbatim "\<forall>"} that both produce the Isabelle
    2.28 +  symbol @{text "\<forall>"} in its Unicode rendering.  Alternatively, symbol
    2.29 +  abbreviations may be used as specified in @{file "~~/etc/symbols"}.
    2.30 +
    2.31 +  \emph{Explicit completion} works via standard jEdit shortcut @{verbatim
    2.32 +  "C+b"}, which is remapped to action @{verbatim "isabelle.complete"}, with a
    2.33 +  fall-back on regular @{verbatim "complete-word"} for non-Isabelle buffers.
    2.34 +
    2.35 +  \emph{Implicit completion} works via keyboard input on text area, with popup
    2.36 +  or immediate insertion into buffer. Plain words require at least 3
    2.37 +  characters to be completed.
    2.38 +
    2.39 +  \emph{Immediate completion} means the (unique) replacement text is inserted
    2.40 +  into the buffer without popup. This mode ignores plain words and requires
    2.41 +  more than one characters for symbol abbreviations. Otherwise it falls back
    2.42 +  on completion popup.
    2.43 +*}
    2.44  
    2.45  
    2.46  chapter {* Known problems and workarounds *}