1.1 --- a/src/Doc/JEdit/JEdit.thy Sun Nov 03 16:49:52 2013 +0100
1.2 +++ b/src/Doc/JEdit/JEdit.thy Sun Nov 03 18:12:23 2013 +0100
1.3 @@ -482,40 +482,107 @@
1.4
1.5 section {* Text completion \label{sec:completion} *}
1.6
1.7 -text {*
1.8 - Text completion works via some light-weight GUI popup, which is triggered by
1.9 - keyboard events during the normal editing process in the main jEdit text
1.10 - area and a few additional text fields. The popup interprets special keys:
1.11 - @{verbatim TAB}, @{verbatim ESCAPE}, @{verbatim UP}, @{verbatim DOWN},
1.12 - @{verbatim PAGE_UP}, @{verbatim PAGE_DOWN}. All other key events are passed
1.13 - to the jEdit text area --- this allows to ignore unwanted completions most
1.14 - of the time and continue typing quickly.
1.15 +text {* \paragraph{Completion tables} are determined statically from
1.16 + the ``outer syntax'' of the underlying edit mode (for theory files
1.17 + this is the syntax of Isar commands) and specifications of Isabelle
1.18 + symbols (see also \secref{sec:symbols}).
1.19
1.20 - Various Isabelle plugin options control the popup behavior and immediate
1.21 - insertion into buffer.
1.22 + Symbols are completed in backslashed forms, e.g.\ @{verbatim
1.23 + "\\"}@{verbatim "forall"} or @{verbatim "\<forall>"} that both produce the
1.24 + Isabelle symbol @{text "\<forall>"} in its Unicode rendering.\footnote{The
1.25 + extra backslash avoids overlap with keywords of the buffer syntax,
1.26 + and facilitates to produce Isabelle symbols in arbitrary syntactic
1.27 + contexts.} Alternatively, symbol abbreviations may be used as
1.28 + specified in @{file "$ISABELLE_HOME/etc/symbols"}.
1.29
1.30 - Isabelle Symbols are completed in backslashed forms, e.g.\ @{verbatim
1.31 - "\\"}@{verbatim "forall"} or @{verbatim "\<forall>"} that both produce the Isabelle
1.32 - symbol @{text "\<forall>"} in its Unicode rendering. Alternatively, symbol
1.33 - abbreviations may be used as specified in @{file
1.34 - "$ISABELLE_HOME/etc/symbols"}.
1.35 + \paragraph{Completion popups} are required in situations of
1.36 + ambiguous completion results or where explicit confirmation is
1.37 + demanded before inserting completed text into the buffer.
1.38
1.39 - \emph{Explicit completion} works via standard jEdit shortcut @{verbatim
1.40 - "C+b"}, which is remapped to action @{verbatim "isabelle.complete"}, with a
1.41 - fall-back on regular @{verbatim "complete-word"} for non-Isabelle buffers.
1.42 + The popup is some minimally invasive GUI component over the text
1.43 + area. It interprets special keys @{verbatim TAB}, @{verbatim
1.44 + ESCAPE}, @{verbatim UP}, @{verbatim DOWN}, @{verbatim PAGE_UP},
1.45 + @{verbatim PAGE_DOWN}, but all other key events are passed to the
1.46 + underlying text area. This allows to ignore unwanted completions
1.47 + most of the time and continue typing quickly.
1.48
1.49 - \emph{Implicit completion} works via keyboard input on text area, with popup
1.50 - or immediate insertion into buffer. Plain words require at least 3
1.51 - characters to be completed.
1.52 + The meaning of special keys is as follows:
1.53
1.54 - \emph{Immediate completion} means the (unique) replacement text is inserted
1.55 - into the buffer without popup. This mode ignores plain words and requires
1.56 - more than one characters for symbol abbreviations. Otherwise it falls back
1.57 - on completion popup.
1.58 + \medskip
1.59 + \begin{tabular}{ll}
1.60 + @{verbatim "TAB"} & select completion \\
1.61 + @{verbatim "ESCAPE"} & dismiss popup \\
1.62 + @{verbatim "UP"} & move up one item \\
1.63 + @{verbatim "DOWN"} & move down one item \\
1.64 + @{verbatim "PAGE_UP"} & move up one page of items \\
1.65 + @{verbatim "PAGE_DOWN"} & move down one page of items \\
1.66 + \end{tabular}
1.67 + \medskip
1.68 +
1.69 + Movement within the popup is only active for multiple items.
1.70 + Otherwise the corresponding key event retains its standard meaning
1.71 + within the underlying text area.
1.72 +
1.73 + \paragraph{Explicit completion} is triggered by the keyword shortcut
1.74 + @{verbatim "C+b"} for action @{verbatim "isabelle.complete"}. This
1.75 + overrides the original jEdit action @{verbatim "complete-word"} on
1.76 + that key sequence, but the latter is used as fall-back for
1.77 + non-Isabelle edit modes. It is also possible to restore the
1.78 + original jEdit keyboard mapping of @{verbatim "complete-word"}.
1.79 +
1.80 + Replacement text is inserted immediately into the buffer, unless
1.81 + ambiguous results demand an explicit popup.
1.82 +
1.83 + \paragraph{Implicit completion} is triggered by regular keyboard
1.84 + input events during of the editing process in the main jEdit text
1.85 + area (and a few additional text fields like the search criterium of
1.86 + the Find panel, see \secref{sec:find}). Implicit completion depends
1.87 + on on further side-conditions:
1.88 +
1.89 + \begin{enumerate}
1.90 +
1.91 + \item The system option @{system_option jedit_completion} needs to
1.92 + be enabled (default).
1.93 +
1.94 + \item Completion of syntax keywords requires at least 3 characters
1.95 + in the text.
1.96 +
1.97 + \item The system option @{system_option jedit_completion} determines
1.98 + an additional delay (0.0 by default), before opening a completion
1.99 + popup.
1.100 +
1.101 + \item The system option @{system_option jedit_completion_immediate}
1.102 + (disabled by default) controls whether replacement text should be
1.103 + inserted immediately without popup, if possible. This only works
1.104 + for Isabelle symbols (\secref{sec:symbols}).
1.105 +
1.106 + \item Completion of symbol abbreviations with only 1 character in
1.107 + the text always enforces and explicit popup, independently of
1.108 + @{system_option jedit_completion_immediate}.
1.109 +
1.110 + \end{enumerate}
1.111 +
1.112 + These completion options may be configured in \emph{Plugin Options /
1.113 + Isabelle / General / Completion}. The default is quite moderate in
1.114 + showing occasional popups and refraining from immediate insertion.
1.115 + An additional of e.g.\ 0.3 seconds will make it even less ambitious.
1.116 +
1.117 + A more aggressive configuration is @{system_option
1.118 + jedit_completion_delay}~@{verbatim "= 0.0"} and @{system_option
1.119 + jedit_completion_immediate}~@{verbatim "= true"}. Thus the editing
1.120 + process becomes more dependent on the system guessing correctly what
1.121 + the user had in mind. It requires some practice and study of the
1.122 + symbol abbreviation tables to be productive in this mode.
1.123 +
1.124 + Unintended completions can be reverted by the regular @{verbatim
1.125 + undo} operation of jEdit. When editing embedded languages such as
1.126 + ML works, it is better to disable either @{system_option
1.127 + jedit_completion} or @{system_option jedit_completion_immediate}
1.128 + temporarily.
1.129 *}
1.130
1.131
1.132 -section {* Isabelle symbols *}
1.133 +section {* Isabelle symbols \label{sec:symbols} *}
1.134
1.135 text {* Isabelle sources consist of \emph{symbols} that extend plain
1.136 ASCII to allow infinitely many mathematical symbols within the
1.137 @@ -810,7 +877,7 @@
1.138 nonetheless, say to remove earlier proof attempts. *}
1.139
1.140
1.141 -section {* Find theorems *}
1.142 +section {* Find theorems \label{sec:find} *}
1.143
1.144 text {* The \emph{Find} panel (\figref{fig:find}) provides an
1.145 independent view for @{command find_theorems}. The main text field