completion popup supports both ENTER and TAB (default);
authorwenzelm
Thu Jul 31 21:29:31 2014 +0200 (2014-07-31)
changeset 578332c2bae3da1c2
parent 57832 5b48f2047c24
child 57834 0d295e339f52
completion popup supports both ENTER and TAB (default);
NEWS
src/Doc/JEdit/JEdit.thy
src/Tools/jEdit/etc/options
src/Tools/jEdit/src/completion_popup.scala
     1.1 --- a/NEWS	Thu Jul 31 20:59:10 2014 +0200
     1.2 +++ b/NEWS	Thu Jul 31 21:29:31 2014 +0200
     1.3 @@ -85,6 +85,9 @@
     1.4  handling and propagation to enclosing text area -- avoid loosing
     1.5  keystrokes with slow / remote graphics displays.
     1.6  
     1.7 +* Completion popup supports both ENTER and TAB (default) to select an
     1.8 +item, depending on Isabelle options.
     1.9 +
    1.10  * Refined insertion of completion items wrt. jEdit text: multiple
    1.11  selections, rectangular selections, rectangular selection as "tall
    1.12  caret".
     2.1 --- a/src/Doc/JEdit/JEdit.thy	Thu Jul 31 20:59:10 2014 +0200
     2.2 +++ b/src/Doc/JEdit/JEdit.thy	Thu Jul 31 21:29:31 2014 +0200
     2.3 @@ -1298,20 +1298,21 @@
     2.4    A \emph{completion popup} is a minimally invasive GUI component over the
     2.5    text area that offers a selection of completion items to be inserted into
     2.6    the text, e.g.\ by mouse clicks. Items are sorted dynamically, according to
     2.7 -  the frequency of selection, with persistent history. The popup interprets
     2.8 -  special keys @{verbatim TAB}, @{verbatim ESCAPE}, @{verbatim UP}, @{verbatim
     2.9 -  DOWN}, @{verbatim PAGE_UP}, @{verbatim PAGE_DOWN}, but all other key events
    2.10 -  are passed to the underlying text area. This allows to ignore unwanted
    2.11 -  completions most of the time and continue typing quickly. Thus the popup
    2.12 -  serves as a mechanism of confirmation of proposed items, but the default is
    2.13 -  to continue without completion.
    2.14 +  the frequency of selection, with persistent history. The popup may interpret
    2.15 +  special keys @{verbatim ENTER}, @{verbatim TAB}, @{verbatim ESCAPE},
    2.16 +  @{verbatim UP}, @{verbatim DOWN}, @{verbatim PAGE_UP}, @{verbatim
    2.17 +  PAGE_DOWN}, but all other key events are passed to the underlying text area.
    2.18 +  This allows to ignore unwanted completions most of the time and continue
    2.19 +  typing quickly. Thus the popup serves as a mechanism of confirmation of
    2.20 +  proposed items, but the default is to continue without completion.
    2.21  
    2.22    The meaning of special keys is as follows:
    2.23  
    2.24    \medskip
    2.25    \begin{tabular}{ll}
    2.26    \textbf{key} & \textbf{action} \\\hline
    2.27 -  @{verbatim "TAB"} & select completion \\
    2.28 +  @{verbatim "ENTER"} & select completion (if @{system_option jedit_completion_select_enter}) \\
    2.29 +  @{verbatim "TAB"} & select completion (if @{system_option jedit_completion_select_tab}) \\
    2.30    @{verbatim "ESCAPE"} & dismiss popup \\
    2.31    @{verbatim "UP"} & move up one item \\
    2.32    @{verbatim "DOWN"} & move down one item \\
    2.33 @@ -1385,6 +1386,11 @@
    2.34    regular jEdit key events (\secref{sec:completion-input}): it allows to
    2.35    disable implicit completion altogether.
    2.36  
    2.37 +  \item @{system_option_def jedit_completion_select_enter} and
    2.38 +  @{system_option_def jedit_completion_select_tab} enable keys to select a
    2.39 +  completion item from the popup (\secref{sec:completion-popup}). Note that a
    2.40 +  regular mouse click on the list of items is always possible.
    2.41 +
    2.42    \item @{system_option_def jedit_completion_context} specifies whether the
    2.43    language context provided by the prover should be used at all. Disabling
    2.44    that option makes completion less ``semantic''. Note that incomplete or
     3.1 --- a/src/Tools/jEdit/etc/options	Thu Jul 31 20:59:10 2014 +0200
     3.2 +++ b/src/Tools/jEdit/etc/options	Thu Jul 31 21:29:31 2014 +0200
     3.3 @@ -42,6 +42,12 @@
     3.4  public option jedit_completion : bool = true
     3.5    -- "enable completion popup"
     3.6  
     3.7 +public option jedit_completion_select_enter : bool = false
     3.8 +  -- "select completion item via ENTER"
     3.9 +
    3.10 +public option jedit_completion_select_tab : bool = true
    3.11 +  -- "select completion item via TAB"
    3.12 +
    3.13  public option jedit_completion_context : bool = true
    3.14    -- "use semantic language context for completion"
    3.15  
     4.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Thu Jul 31 20:59:10 2014 +0200
     4.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Thu Jul 31 21:29:31 2014 +0200
     4.3 @@ -702,7 +702,10 @@
     4.4          {
     4.5            if (!e.isConsumed) {
     4.6              e.getKeyCode match {
     4.7 -              case KeyEvent.VK_TAB =>
     4.8 +              case KeyEvent.VK_ENTER if PIDE.options.bool("jedit_completion_select_enter") =>
     4.9 +                if (complete_selected()) e.consume
    4.10 +                hide_popup()
    4.11 +              case KeyEvent.VK_TAB if PIDE.options.bool("jedit_completion_select_tab") =>
    4.12                  if (complete_selected()) e.consume
    4.13                  hide_popup()
    4.14                case KeyEvent.VK_ESCAPE =>