--- a/NEWS Thu Jul 31 20:59:10 2014 +0200
+++ b/NEWS Thu Jul 31 21:29:31 2014 +0200
@@ -85,6 +85,9 @@
handling and propagation to enclosing text area -- avoid loosing
keystrokes with slow / remote graphics displays.
+* Completion popup supports both ENTER and TAB (default) to select an
+item, depending on Isabelle options.
+
* Refined insertion of completion items wrt. jEdit text: multiple
selections, rectangular selections, rectangular selection as "tall
caret".
--- a/src/Doc/JEdit/JEdit.thy Thu Jul 31 20:59:10 2014 +0200
+++ b/src/Doc/JEdit/JEdit.thy Thu Jul 31 21:29:31 2014 +0200
@@ -1298,20 +1298,21 @@
A \emph{completion popup} is a minimally invasive GUI component over the
text area that offers a selection of completion items to be inserted into
the text, e.g.\ by mouse clicks. Items are sorted dynamically, according to
- the frequency of selection, with persistent history. The popup interprets
- special keys @{verbatim TAB}, @{verbatim ESCAPE}, @{verbatim UP}, @{verbatim
- DOWN}, @{verbatim PAGE_UP}, @{verbatim PAGE_DOWN}, but all other key events
- are passed to the underlying text area. This allows to ignore unwanted
- completions most of the time and continue typing quickly. Thus the popup
- serves as a mechanism of confirmation of proposed items, but the default is
- to continue without completion.
+ the frequency of selection, with persistent history. The popup may interpret
+ special keys @{verbatim ENTER}, @{verbatim TAB}, @{verbatim ESCAPE},
+ @{verbatim UP}, @{verbatim DOWN}, @{verbatim PAGE_UP}, @{verbatim
+ PAGE_DOWN}, but all other key events are passed to the underlying text area.
+ This allows to ignore unwanted completions most of the time and continue
+ typing quickly. Thus the popup serves as a mechanism of confirmation of
+ proposed items, but the default is to continue without completion.
The meaning of special keys is as follows:
\medskip
\begin{tabular}{ll}
\textbf{key} & \textbf{action} \\\hline
- @{verbatim "TAB"} & select completion \\
+ @{verbatim "ENTER"} & select completion (if @{system_option jedit_completion_select_enter}) \\
+ @{verbatim "TAB"} & select completion (if @{system_option jedit_completion_select_tab}) \\
@{verbatim "ESCAPE"} & dismiss popup \\
@{verbatim "UP"} & move up one item \\
@{verbatim "DOWN"} & move down one item \\
@@ -1385,6 +1386,11 @@
regular jEdit key events (\secref{sec:completion-input}): it allows to
disable implicit completion altogether.
+ \item @{system_option_def jedit_completion_select_enter} and
+ @{system_option_def jedit_completion_select_tab} enable keys to select a
+ completion item from the popup (\secref{sec:completion-popup}). Note that a
+ regular mouse click on the list of items is always possible.
+
\item @{system_option_def jedit_completion_context} specifies whether the
language context provided by the prover should be used at all. Disabling
that option makes completion less ``semantic''. Note that incomplete or
--- a/src/Tools/jEdit/etc/options Thu Jul 31 20:59:10 2014 +0200
+++ b/src/Tools/jEdit/etc/options Thu Jul 31 21:29:31 2014 +0200
@@ -42,6 +42,12 @@
public option jedit_completion : bool = true
-- "enable completion popup"
+public option jedit_completion_select_enter : bool = false
+ -- "select completion item via ENTER"
+
+public option jedit_completion_select_tab : bool = true
+ -- "select completion item via TAB"
+
public option jedit_completion_context : bool = true
-- "use semantic language context for completion"
--- a/src/Tools/jEdit/src/completion_popup.scala Thu Jul 31 20:59:10 2014 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala Thu Jul 31 21:29:31 2014 +0200
@@ -702,7 +702,10 @@
{
if (!e.isConsumed) {
e.getKeyCode match {
- case KeyEvent.VK_TAB =>
+ case KeyEvent.VK_ENTER if PIDE.options.bool("jedit_completion_select_enter") =>
+ if (complete_selected()) e.consume
+ hide_popup()
+ case KeyEvent.VK_TAB if PIDE.options.bool("jedit_completion_select_tab") =>
if (complete_selected()) e.consume
hide_popup()
case KeyEvent.VK_ESCAPE =>