src/Tools/jEdit/src/completion_popup.scala
author wenzelm
Sat, 03 May 2014 20:20:55 +0200
changeset 56841 bc6faeadbf82
parent 56840 879fe16bd27c
child 56842 b6e266574b26
permissions -rw-r--r--
reduced cluttering of popups;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
53023
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
     1
/*  Title:      Tools/jEdit/src/completion_popup.scala
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
     3
53246
8d34caf5bf82 more elementary Popup via JLayeredPane -- avoid javax.swing.PopupFactory with its many problems and dangers of accidental HeavyWeightPopup (especially on Mac OS X);
wenzelm
parents: 53244
diff changeset
     4
Completion popup.
53023
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
     5
*/
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
     6
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
     7
package isabelle.jedit
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
     8
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
     9
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
    10
import isabelle._
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
    11
53297
64c31de7f21c border as for Pretty_Tooltip;
wenzelm
parents: 53296
diff changeset
    12
import java.awt.{Color, Font, Point, BorderLayout, Dimension}
53784
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
    13
import java.awt.event.{KeyEvent, MouseEvent, MouseAdapter, FocusAdapter, FocusEvent}
53246
8d34caf5bf82 more elementary Popup via JLayeredPane -- avoid javax.swing.PopupFactory with its many problems and dangers of accidental HeavyWeightPopup (especially on Mac OS X);
wenzelm
parents: 53244
diff changeset
    14
import javax.swing.{JPanel, JComponent, JLayeredPane, SwingUtilities}
53297
64c31de7f21c border as for Pretty_Tooltip;
wenzelm
parents: 53296
diff changeset
    15
import javax.swing.border.LineBorder
53848
8d7029eb0c31 disable standard behaviour of Mac OS X text field (i.e. select-all after focus gain) in order to make completion work more smoothly;
wenzelm
parents: 53784
diff changeset
    16
import javax.swing.text.DefaultCaret
53023
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
    17
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
    18
import scala.swing.{ListView, ScrollPane}
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
    19
import scala.swing.event.MouseClicked
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
    20
53784
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
    21
import org.gjt.sp.jedit.View
56325
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing;
wenzelm
parents: 56197
diff changeset
    22
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, Selection}
53784
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
    23
import org.gjt.sp.jedit.gui.{HistoryTextField, KeyEventWorkaround}
53023
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
    24
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
    25
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
    26
object Completion_Popup
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
    27
{
55978
56645c447ee9 tuned description and its rendering;
wenzelm
parents: 55914
diff changeset
    28
  /** items with HTML rendering **/
56645c447ee9 tuned description and its rendering;
wenzelm
parents: 55914
diff changeset
    29
56645c447ee9 tuned description and its rendering;
wenzelm
parents: 55914
diff changeset
    30
  private class Item(val item: Completion.Item)
56645c447ee9 tuned description and its rendering;
wenzelm
parents: 55914
diff changeset
    31
  {
56645c447ee9 tuned description and its rendering;
wenzelm
parents: 55914
diff changeset
    32
    private val html =
56645c447ee9 tuned description and its rendering;
wenzelm
parents: 55914
diff changeset
    33
      item.description match {
56645c447ee9 tuned description and its rendering;
wenzelm
parents: 55914
diff changeset
    34
        case a :: bs =>
56645c447ee9 tuned description and its rendering;
wenzelm
parents: 55914
diff changeset
    35
          "<html><b>" + HTML.encode(a) + "</b>" +
56645c447ee9 tuned description and its rendering;
wenzelm
parents: 55914
diff changeset
    36
            HTML.encode(bs.map(" " + _).mkString) + "</html>"
56645c447ee9 tuned description and its rendering;
wenzelm
parents: 55914
diff changeset
    37
        case Nil => ""
56645c447ee9 tuned description and its rendering;
wenzelm
parents: 55914
diff changeset
    38
      }
56645c447ee9 tuned description and its rendering;
wenzelm
parents: 55914
diff changeset
    39
    override def toString: String = html
56645c447ee9 tuned description and its rendering;
wenzelm
parents: 55914
diff changeset
    40
  }
56645c447ee9 tuned description and its rendering;
wenzelm
parents: 55914
diff changeset
    41
56645c447ee9 tuned description and its rendering;
wenzelm
parents: 55914
diff changeset
    42
56645c447ee9 tuned description and its rendering;
wenzelm
parents: 55914
diff changeset
    43
53784
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
    44
  /** jEdit text area **/
53235
1b6a44859549 register single instance within root, in order to get rid of old popup as user continues typing;
wenzelm
parents: 53234
diff changeset
    45
53242
142f4fff4e40 tuned signature;
wenzelm
parents: 53237
diff changeset
    46
  object Text_Area
53233
4b422e5d64fd some actual completion via outer syntax;
wenzelm
parents: 53232
diff changeset
    47
  {
53274
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
    48
    private val key = new Object
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
    49
55712
e757e8c8d8ea tuned signature -- weaker type requirement;
wenzelm
parents: 55711
diff changeset
    50
    def apply(text_area: TextArea): Option[Completion_Popup.Text_Area] =
e757e8c8d8ea tuned signature -- weaker type requirement;
wenzelm
parents: 55711
diff changeset
    51
    {
56662
f373fb77e0a4 avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
wenzelm
parents: 56606
diff changeset
    52
      Swing_Thread.require {}
53274
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
    53
      text_area.getClientProperty(key) match {
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
    54
        case text_area_completion: Completion_Popup.Text_Area => Some(text_area_completion)
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
    55
        case _ => None
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
    56
      }
55712
e757e8c8d8ea tuned signature -- weaker type requirement;
wenzelm
parents: 55711
diff changeset
    57
    }
53274
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
    58
55712
e757e8c8d8ea tuned signature -- weaker type requirement;
wenzelm
parents: 55711
diff changeset
    59
    def active_range(text_area: TextArea): Option[Text.Range] =
e757e8c8d8ea tuned signature -- weaker type requirement;
wenzelm
parents: 55711
diff changeset
    60
      apply(text_area) match {
e757e8c8d8ea tuned signature -- weaker type requirement;
wenzelm
parents: 55711
diff changeset
    61
        case Some(text_area_completion) => text_area_completion.active_range
e757e8c8d8ea tuned signature -- weaker type requirement;
wenzelm
parents: 55711
diff changeset
    62
        case None => None
55711
9e3d64e5919a paint completion range of active popup;
wenzelm
parents: 55693
diff changeset
    63
      }
9e3d64e5919a paint completion range of active popup;
wenzelm
parents: 55693
diff changeset
    64
56586
5ef60881681d explicit menu action to complete word;
wenzelm
parents: 56576
diff changeset
    65
    def action(text_area: TextArea, word_only: Boolean): Boolean =
56170
638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time;
wenzelm
parents: 55978
diff changeset
    66
      apply(text_area) match {
638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time;
wenzelm
parents: 55978
diff changeset
    67
        case Some(text_area_completion) =>
638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time;
wenzelm
parents: 55978
diff changeset
    68
          if (text_area_completion.active_range.isDefined)
56586
5ef60881681d explicit menu action to complete word;
wenzelm
parents: 56576
diff changeset
    69
            text_area_completion.action(word_only = word_only)
56177
bfa9dfb722de proper flags for main action (amending 638b29331549);
wenzelm
parents: 56175
diff changeset
    70
          else
56586
5ef60881681d explicit menu action to complete word;
wenzelm
parents: 56576
diff changeset
    71
            text_area_completion.action(immediate = true, explicit = true, word_only = word_only)
56170
638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time;
wenzelm
parents: 55978
diff changeset
    72
          true
638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time;
wenzelm
parents: 55978
diff changeset
    73
        case None => false
638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time;
wenzelm
parents: 55978
diff changeset
    74
      }
638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time;
wenzelm
parents: 55978
diff changeset
    75
53274
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
    76
    def exit(text_area: JEditTextArea)
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
    77
    {
56662
f373fb77e0a4 avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
wenzelm
parents: 56606
diff changeset
    78
      Swing_Thread.require {}
53274
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
    79
      apply(text_area) match {
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
    80
        case None =>
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
    81
        case Some(text_area_completion) =>
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
    82
          text_area_completion.deactivate()
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
    83
          text_area.putClientProperty(key, null)
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
    84
      }
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
    85
    }
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
    86
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
    87
    def init(text_area: JEditTextArea): Completion_Popup.Text_Area =
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
    88
    {
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
    89
      exit(text_area)
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
    90
      val text_area_completion = new Text_Area(text_area)
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
    91
      text_area.putClientProperty(key, text_area_completion)
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
    92
      text_area_completion.activate()
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
    93
      text_area_completion
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
    94
    }
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
    95
55712
e757e8c8d8ea tuned signature -- weaker type requirement;
wenzelm
parents: 55711
diff changeset
    96
    def dismissed(text_area: TextArea): Boolean =
53274
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
    97
    {
56662
f373fb77e0a4 avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
wenzelm
parents: 56606
diff changeset
    98
      Swing_Thread.require {}
53274
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
    99
      apply(text_area) match {
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
   100
        case Some(text_area_completion) => text_area_completion.dismissed()
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
   101
        case None => false
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
   102
      }
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
   103
    }
53272
0dfd78ff7696 more abstract Completion_Popup.Text_Area;
wenzelm
parents: 53247
diff changeset
   104
  }
0dfd78ff7696 more abstract Completion_Popup.Text_Area;
wenzelm
parents: 53247
diff changeset
   105
53274
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
   106
  class Text_Area private(text_area: JEditTextArea)
53272
0dfd78ff7696 more abstract Completion_Popup.Text_Area;
wenzelm
parents: 53247
diff changeset
   107
  {
55711
9e3d64e5919a paint completion range of active popup;
wenzelm
parents: 55693
diff changeset
   108
    // owned by Swing thread
53272
0dfd78ff7696 more abstract Completion_Popup.Text_Area;
wenzelm
parents: 53247
diff changeset
   109
    private var completion_popup: Option[Completion_Popup] = None
0dfd78ff7696 more abstract Completion_Popup.Text_Area;
wenzelm
parents: 53247
diff changeset
   110
55711
9e3d64e5919a paint completion range of active popup;
wenzelm
parents: 55693
diff changeset
   111
    def active_range: Option[Text.Range] =
9e3d64e5919a paint completion range of active popup;
wenzelm
parents: 55693
diff changeset
   112
      completion_popup match {
56605
wenzelm
parents: 56593
diff changeset
   113
        case Some(completion) => completion.active_range
55711
9e3d64e5919a paint completion range of active popup;
wenzelm
parents: 55693
diff changeset
   114
        case None => None
9e3d64e5919a paint completion range of active popup;
wenzelm
parents: 55693
diff changeset
   115
      }
9e3d64e5919a paint completion range of active popup;
wenzelm
parents: 55693
diff changeset
   116
53272
0dfd78ff7696 more abstract Completion_Popup.Text_Area;
wenzelm
parents: 53247
diff changeset
   117
55747
bef19c929ba5 more completion rendering: active, semantic, syntactic;
wenzelm
parents: 55712
diff changeset
   118
    /* rendering */
bef19c929ba5 more completion rendering: active, semantic, syntactic;
wenzelm
parents: 55712
diff changeset
   119
bef19c929ba5 more completion rendering: active, semantic, syntactic;
wenzelm
parents: 55712
diff changeset
   120
    def rendering(rendering: Rendering, line_range: Text.Range): Option[Text.Info[Color]] =
bef19c929ba5 more completion rendering: active, semantic, syntactic;
wenzelm
parents: 55712
diff changeset
   121
    {
bef19c929ba5 more completion rendering: active, semantic, syntactic;
wenzelm
parents: 55712
diff changeset
   122
      active_range match {
bef19c929ba5 more completion rendering: active, semantic, syntactic;
wenzelm
parents: 55712
diff changeset
   123
        case Some(range) => range.try_restrict(line_range)
bef19c929ba5 more completion rendering: active, semantic, syntactic;
wenzelm
parents: 55712
diff changeset
   124
        case None =>
55767
96ddf9bf12ac more precise before_caret_range (looking both in space and time);
wenzelm
parents: 55752
diff changeset
   125
          if (line_range.contains(text_area.getCaretPosition)) {
56593
0ea7c84110ac back to unrestricted before_caret_range, which is important for quick editing at the end of line (amending 83777a91f5de);
wenzelm
parents: 56589
diff changeset
   126
            JEdit_Lib.before_caret_range(text_area, rendering).try_restrict(line_range) match {
55747
bef19c929ba5 more completion rendering: active, semantic, syntactic;
wenzelm
parents: 55712
diff changeset
   127
              case Some(range) if !range.is_singularity =>
56173
62f10624339a tuned signature;
wenzelm
parents: 56171
diff changeset
   128
                rendering.semantic_completion(range) match {
56175
79c29244b377 merge semantic and syntax completion;
wenzelm
parents: 56173
diff changeset
   129
                  case Some(Text.Info(_, Completion.No_Completion)) => None
79c29244b377 merge semantic and syntax completion;
wenzelm
parents: 56173
diff changeset
   130
                  case Some(Text.Info(range1, _: Completion.Names)) => Some(range1)
55747
bef19c929ba5 more completion rendering: active, semantic, syntactic;
wenzelm
parents: 55712
diff changeset
   131
                  case None =>
56175
79c29244b377 merge semantic and syntax completion;
wenzelm
parents: 56173
diff changeset
   132
                    syntax_completion(Completion.History.empty, false, Some(rendering)).map(_.range)
55747
bef19c929ba5 more completion rendering: active, semantic, syntactic;
wenzelm
parents: 55712
diff changeset
   133
                }
bef19c929ba5 more completion rendering: active, semantic, syntactic;
wenzelm
parents: 55712
diff changeset
   134
              case _ => None
bef19c929ba5 more completion rendering: active, semantic, syntactic;
wenzelm
parents: 55712
diff changeset
   135
            }
bef19c929ba5 more completion rendering: active, semantic, syntactic;
wenzelm
parents: 55712
diff changeset
   136
          }
bef19c929ba5 more completion rendering: active, semantic, syntactic;
wenzelm
parents: 55712
diff changeset
   137
          else None
bef19c929ba5 more completion rendering: active, semantic, syntactic;
wenzelm
parents: 55712
diff changeset
   138
      }
bef19c929ba5 more completion rendering: active, semantic, syntactic;
wenzelm
parents: 55712
diff changeset
   139
    }.map(range => Text.Info(range, rendering.completion_color))
bef19c929ba5 more completion rendering: active, semantic, syntactic;
wenzelm
parents: 55712
diff changeset
   140
bef19c929ba5 more completion rendering: active, semantic, syntactic;
wenzelm
parents: 55712
diff changeset
   141
bef19c929ba5 more completion rendering: active, semantic, syntactic;
wenzelm
parents: 55712
diff changeset
   142
    /* syntax completion */
bef19c929ba5 more completion rendering: active, semantic, syntactic;
wenzelm
parents: 55712
diff changeset
   143
bef19c929ba5 more completion rendering: active, semantic, syntactic;
wenzelm
parents: 55712
diff changeset
   144
    def syntax_completion(
56175
79c29244b377 merge semantic and syntax completion;
wenzelm
parents: 56173
diff changeset
   145
      history: Completion.History,
79c29244b377 merge semantic and syntax completion;
wenzelm
parents: 56173
diff changeset
   146
      explicit: Boolean,
79c29244b377 merge semantic and syntax completion;
wenzelm
parents: 56173
diff changeset
   147
      opt_rendering: Option[Rendering]): Option[Completion.Result] =
55747
bef19c929ba5 more completion rendering: active, semantic, syntactic;
wenzelm
parents: 55712
diff changeset
   148
    {
bef19c929ba5 more completion rendering: active, semantic, syntactic;
wenzelm
parents: 55712
diff changeset
   149
      val buffer = text_area.getBuffer
bef19c929ba5 more completion rendering: active, semantic, syntactic;
wenzelm
parents: 55712
diff changeset
   150
      val decode = Isabelle_Encoding.is_active(buffer)
bef19c929ba5 more completion rendering: active, semantic, syntactic;
wenzelm
parents: 55712
diff changeset
   151
bef19c929ba5 more completion rendering: active, semantic, syntactic;
wenzelm
parents: 55712
diff changeset
   152
      Isabelle.mode_syntax(JEdit_Lib.buffer_mode(buffer)) match {
bef19c929ba5 more completion rendering: active, semantic, syntactic;
wenzelm
parents: 55712
diff changeset
   153
        case Some(syntax) =>
bef19c929ba5 more completion rendering: active, semantic, syntactic;
wenzelm
parents: 55712
diff changeset
   154
          val context =
56587
83777a91f5de clarified before_caret_range: prevent continuation on next line;
wenzelm
parents: 56586
diff changeset
   155
            (for {
83777a91f5de clarified before_caret_range: prevent continuation on next line;
wenzelm
parents: 56586
diff changeset
   156
              rendering <- opt_rendering
56593
0ea7c84110ac back to unrestricted before_caret_range, which is important for quick editing at the end of line (amending 83777a91f5de);
wenzelm
parents: 56589
diff changeset
   157
              range = JEdit_Lib.before_caret_range(text_area, rendering)
56587
83777a91f5de clarified before_caret_range: prevent continuation on next line;
wenzelm
parents: 56586
diff changeset
   158
              context <- rendering.language_context(range)
83777a91f5de clarified before_caret_range: prevent continuation on next line;
wenzelm
parents: 56586
diff changeset
   159
            } yield context) getOrElse syntax.language_context
55747
bef19c929ba5 more completion rendering: active, semantic, syntactic;
wenzelm
parents: 55712
diff changeset
   160
56589
71c5d1f516c0 more robust JEdit_Lib.line_range, according to usual jEdit confusion at end of last line;
wenzelm
parents: 56587
diff changeset
   161
          val caret = text_area.getCaretPosition
71c5d1f516c0 more robust JEdit_Lib.line_range, according to usual jEdit confusion at end of last line;
wenzelm
parents: 56587
diff changeset
   162
          val line_range = JEdit_Lib.line_range(buffer, text_area.getCaretLine)
71c5d1f516c0 more robust JEdit_Lib.line_range, according to usual jEdit confusion at end of last line;
wenzelm
parents: 56587
diff changeset
   163
          val line_start = line_range.start
71c5d1f516c0 more robust JEdit_Lib.line_range, according to usual jEdit confusion at end of last line;
wenzelm
parents: 56587
diff changeset
   164
          for {
71c5d1f516c0 more robust JEdit_Lib.line_range, according to usual jEdit confusion at end of last line;
wenzelm
parents: 56587
diff changeset
   165
            line_text <- JEdit_Lib.try_get_text(buffer, line_range)
71c5d1f516c0 more robust JEdit_Lib.line_range, according to usual jEdit confusion at end of last line;
wenzelm
parents: 56587
diff changeset
   166
            result <-
71c5d1f516c0 more robust JEdit_Lib.line_range, according to usual jEdit confusion at end of last line;
wenzelm
parents: 56587
diff changeset
   167
              syntax.completion.complete(
71c5d1f516c0 more robust JEdit_Lib.line_range, according to usual jEdit confusion at end of last line;
wenzelm
parents: 56587
diff changeset
   168
                history, decode, explicit, line_start, line_text, caret - line_start, false, context)
71c5d1f516c0 more robust JEdit_Lib.line_range, according to usual jEdit confusion at end of last line;
wenzelm
parents: 56587
diff changeset
   169
          } yield result
55747
bef19c929ba5 more completion rendering: active, semantic, syntactic;
wenzelm
parents: 55712
diff changeset
   170
bef19c929ba5 more completion rendering: active, semantic, syntactic;
wenzelm
parents: 55712
diff changeset
   171
        case None => None
bef19c929ba5 more completion rendering: active, semantic, syntactic;
wenzelm
parents: 55712
diff changeset
   172
      }
bef19c929ba5 more completion rendering: active, semantic, syntactic;
wenzelm
parents: 55712
diff changeset
   173
    }
bef19c929ba5 more completion rendering: active, semantic, syntactic;
wenzelm
parents: 55712
diff changeset
   174
bef19c929ba5 more completion rendering: active, semantic, syntactic;
wenzelm
parents: 55712
diff changeset
   175
56564
94c55cc73747 added spell-checker completion dialog, without counting frequency of items due to empty name;
wenzelm
parents: 56326
diff changeset
   176
    /* spell-checker completion */
94c55cc73747 added spell-checker completion dialog, without counting frequency of items due to empty name;
wenzelm
parents: 56326
diff changeset
   177
94c55cc73747 added spell-checker completion dialog, without counting frequency of items due to empty name;
wenzelm
parents: 56326
diff changeset
   178
    def spell_checker_completion(rendering: Rendering): Option[Completion.Result] =
56587
83777a91f5de clarified before_caret_range: prevent continuation on next line;
wenzelm
parents: 56586
diff changeset
   179
    {
83777a91f5de clarified before_caret_range: prevent continuation on next line;
wenzelm
parents: 56586
diff changeset
   180
      for {
83777a91f5de clarified before_caret_range: prevent continuation on next line;
wenzelm
parents: 56586
diff changeset
   181
        spell_checker <- PIDE.spell_checker.get
56593
0ea7c84110ac back to unrestricted before_caret_range, which is important for quick editing at the end of line (amending 83777a91f5de);
wenzelm
parents: 56589
diff changeset
   182
        range = JEdit_Lib.before_caret_range(text_area, rendering)
0ea7c84110ac back to unrestricted before_caret_range, which is important for quick editing at the end of line (amending 83777a91f5de);
wenzelm
parents: 56589
diff changeset
   183
        word <- Spell_Checker.current_word(text_area, rendering, range)
0ea7c84110ac back to unrestricted before_caret_range, which is important for quick editing at the end of line (amending 83777a91f5de);
wenzelm
parents: 56589
diff changeset
   184
        words = spell_checker.complete(word.info)
56587
83777a91f5de clarified before_caret_range: prevent continuation on next line;
wenzelm
parents: 56586
diff changeset
   185
        if !words.isEmpty
83777a91f5de clarified before_caret_range: prevent continuation on next line;
wenzelm
parents: 56586
diff changeset
   186
        descr = "(from dictionary " + quote(spell_checker.toString) + ")"
56593
0ea7c84110ac back to unrestricted before_caret_range, which is important for quick editing at the end of line (amending 83777a91f5de);
wenzelm
parents: 56589
diff changeset
   187
        items =
0ea7c84110ac back to unrestricted before_caret_range, which is important for quick editing at the end of line (amending 83777a91f5de);
wenzelm
parents: 56589
diff changeset
   188
          words.map(w => Completion.Item(word.range, word.info, "", List(w, descr), w, 0, false))
0ea7c84110ac back to unrestricted before_caret_range, which is important for quick editing at the end of line (amending 83777a91f5de);
wenzelm
parents: 56589
diff changeset
   189
      } yield Completion.Result(word.range, word.info, false, items)
56587
83777a91f5de clarified before_caret_range: prevent continuation on next line;
wenzelm
parents: 56586
diff changeset
   190
    }
56564
94c55cc73747 added spell-checker completion dialog, without counting frequency of items due to empty name;
wenzelm
parents: 56326
diff changeset
   191
94c55cc73747 added spell-checker completion dialog, without counting frequency of items due to empty name;
wenzelm
parents: 56326
diff changeset
   192
56170
638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time;
wenzelm
parents: 55978
diff changeset
   193
    /* completion action: text area */
53273
473ea1ed7503 some completion options;
wenzelm
parents: 53272
diff changeset
   194
53275
b34aac6511ab tuned signature;
wenzelm
parents: 53274
diff changeset
   195
    private def insert(item: Completion.Item)
53242
142f4fff4e40 tuned signature;
wenzelm
parents: 53237
diff changeset
   196
    {
56662
f373fb77e0a4 avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
wenzelm
parents: 56606
diff changeset
   197
      Swing_Thread.require {}
53023
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   198
53242
142f4fff4e40 tuned signature;
wenzelm
parents: 53237
diff changeset
   199
      val buffer = text_area.getBuffer
55692
19e8b00684f7 more explicit Completion.Item.range, independently of caret;
wenzelm
parents: 55690
diff changeset
   200
      val range = item.range
19e8b00684f7 more explicit Completion.Item.range, independently of caret;
wenzelm
parents: 55690
diff changeset
   201
      if (buffer.isEditable && range.length > 0) {
53242
142f4fff4e40 tuned signature;
wenzelm
parents: 53237
diff changeset
   202
        JEdit_Lib.buffer_edit(buffer) {
55692
19e8b00684f7 more explicit Completion.Item.range, independently of caret;
wenzelm
parents: 55690
diff changeset
   203
          JEdit_Lib.try_get_text(buffer, range) match {
53242
142f4fff4e40 tuned signature;
wenzelm
parents: 53237
diff changeset
   204
            case Some(text) if text == item.original =>
56325
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing;
wenzelm
parents: 56197
diff changeset
   205
              text_area.getSelectionAtOffset(text_area.getCaretPosition) match {
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing;
wenzelm
parents: 56197
diff changeset
   206
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing;
wenzelm
parents: 56197
diff changeset
   207
                /*rectangular selection as "tall caret"*/
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing;
wenzelm
parents: 56197
diff changeset
   208
                case selection : Selection.Rect
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing;
wenzelm
parents: 56197
diff changeset
   209
                if selection.getStart(buffer, text_area.getCaretLine) == range.stop =>
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing;
wenzelm
parents: 56197
diff changeset
   210
                  text_area.moveCaretPosition(range.stop)
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing;
wenzelm
parents: 56197
diff changeset
   211
                  (0 until Character.codePointCount(item.original, 0, item.original.length))
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing;
wenzelm
parents: 56197
diff changeset
   212
                    .foreach(_ => text_area.backspace())
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing;
wenzelm
parents: 56197
diff changeset
   213
                  text_area.setSelectedText(selection, item.replacement)
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing;
wenzelm
parents: 56197
diff changeset
   214
                  text_area.moveCaretPosition(text_area.getCaretPosition + item.move)
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing;
wenzelm
parents: 56197
diff changeset
   215
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing;
wenzelm
parents: 56197
diff changeset
   216
                /*other selections: rectangular, multiple range, ...*/
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing;
wenzelm
parents: 56197
diff changeset
   217
                case selection
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing;
wenzelm
parents: 56197
diff changeset
   218
                if selection != null &&
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing;
wenzelm
parents: 56197
diff changeset
   219
                    selection.getStart(buffer, text_area.getCaretLine) == range.start &&
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing;
wenzelm
parents: 56197
diff changeset
   220
                    selection.getEnd(buffer, text_area.getCaretLine) == range.stop =>
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing;
wenzelm
parents: 56197
diff changeset
   221
                  text_area.moveCaretPosition(range.stop + item.move)
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing;
wenzelm
parents: 56197
diff changeset
   222
                  text_area.getSelection.foreach(text_area.setSelectedText(_, item.replacement))
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing;
wenzelm
parents: 56197
diff changeset
   223
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing;
wenzelm
parents: 56197
diff changeset
   224
                /*no selection*/
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing;
wenzelm
parents: 56197
diff changeset
   225
                case _ =>
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing;
wenzelm
parents: 56197
diff changeset
   226
                  buffer.remove(range.start, range.length)
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing;
wenzelm
parents: 56197
diff changeset
   227
                  buffer.insert(range.start, item.replacement)
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing;
wenzelm
parents: 56197
diff changeset
   228
                  text_area.moveCaretPosition(range.start + item.replacement.length + item.move)
ffbfc92e6508 special treatment for various kinds of selections: imitate normal flow of editing;
wenzelm
parents: 56197
diff changeset
   229
              }
53242
142f4fff4e40 tuned signature;
wenzelm
parents: 53237
diff changeset
   230
            case _ =>
142f4fff4e40 tuned signature;
wenzelm
parents: 53237
diff changeset
   231
          }
53233
4b422e5d64fd some actual completion via outer syntax;
wenzelm
parents: 53232
diff changeset
   232
        }
4b422e5d64fd some actual completion via outer syntax;
wenzelm
parents: 53232
diff changeset
   233
      }
4b422e5d64fd some actual completion via outer syntax;
wenzelm
parents: 53232
diff changeset
   234
    }
53242
142f4fff4e40 tuned signature;
wenzelm
parents: 53237
diff changeset
   235
56586
5ef60881681d explicit menu action to complete word;
wenzelm
parents: 56576
diff changeset
   236
    def action(
5ef60881681d explicit menu action to complete word;
wenzelm
parents: 56576
diff changeset
   237
      immediate: Boolean = false,
5ef60881681d explicit menu action to complete word;
wenzelm
parents: 56576
diff changeset
   238
      explicit: Boolean = false,
5ef60881681d explicit menu action to complete word;
wenzelm
parents: 56576
diff changeset
   239
      delayed: Boolean = false,
5ef60881681d explicit menu action to complete word;
wenzelm
parents: 56576
diff changeset
   240
      word_only: Boolean = false): Boolean =
53292
f567c1c7b180 option to insert unique completion immediately into buffer;
wenzelm
parents: 53275
diff changeset
   241
    {
f567c1c7b180 option to insert unique completion immediately into buffer;
wenzelm
parents: 53275
diff changeset
   242
      val view = text_area.getView
f567c1c7b180 option to insert unique completion immediately into buffer;
wenzelm
parents: 53275
diff changeset
   243
      val layered = view.getLayeredPane
f567c1c7b180 option to insert unique completion immediately into buffer;
wenzelm
parents: 53275
diff changeset
   244
      val buffer = text_area.getBuffer
f567c1c7b180 option to insert unique completion immediately into buffer;
wenzelm
parents: 53275
diff changeset
   245
      val painter = text_area.getPainter
53273
473ea1ed7503 some completion options;
wenzelm
parents: 53272
diff changeset
   246
55693
93ba0085e888 try explicit semantic completion before syntax completion;
wenzelm
parents: 55692
diff changeset
   247
      val history = PIDE.completion_history.value
93ba0085e888 try explicit semantic completion before syntax completion;
wenzelm
parents: 55692
diff changeset
   248
      val decode = Isabelle_Encoding.is_active(buffer)
93ba0085e888 try explicit semantic completion before syntax completion;
wenzelm
parents: 55692
diff changeset
   249
93ba0085e888 try explicit semantic completion before syntax completion;
wenzelm
parents: 55692
diff changeset
   250
      def open_popup(result: Completion.Result)
93ba0085e888 try explicit semantic completion before syntax completion;
wenzelm
parents: 55692
diff changeset
   251
      {
93ba0085e888 try explicit semantic completion before syntax completion;
wenzelm
parents: 55692
diff changeset
   252
        val font =
55825
694833e3e4a0 tuned signature -- separate module Font_Info;
wenzelm
parents: 55813
diff changeset
   253
          painter.getFont.deriveFont(
694833e3e4a0 tuned signature -- separate module Font_Info;
wenzelm
parents: 55813
diff changeset
   254
            Font_Info.main_size(PIDE.options.real("jedit_popup_font_scale")))
55693
93ba0085e888 try explicit semantic completion before syntax completion;
wenzelm
parents: 55692
diff changeset
   255
55711
9e3d64e5919a paint completion range of active popup;
wenzelm
parents: 55693
diff changeset
   256
        val range = result.range
9e3d64e5919a paint completion range of active popup;
wenzelm
parents: 55693
diff changeset
   257
9e3d64e5919a paint completion range of active popup;
wenzelm
parents: 55693
diff changeset
   258
        val loc1 = text_area.offsetToXY(range.start)
55693
93ba0085e888 try explicit semantic completion before syntax completion;
wenzelm
parents: 55692
diff changeset
   259
        if (loc1 != null) {
93ba0085e888 try explicit semantic completion before syntax completion;
wenzelm
parents: 55692
diff changeset
   260
          val loc2 =
93ba0085e888 try explicit semantic completion before syntax completion;
wenzelm
parents: 55692
diff changeset
   261
            SwingUtilities.convertPoint(painter,
93ba0085e888 try explicit semantic completion before syntax completion;
wenzelm
parents: 55692
diff changeset
   262
              loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered)
93ba0085e888 try explicit semantic completion before syntax completion;
wenzelm
parents: 55692
diff changeset
   263
55978
56645c447ee9 tuned description and its rendering;
wenzelm
parents: 55914
diff changeset
   264
          val items = result.items.map(new Item(_))
55693
93ba0085e888 try explicit semantic completion before syntax completion;
wenzelm
parents: 55692
diff changeset
   265
          val completion =
56197
416f7a00e4cb back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups;
wenzelm
parents: 56177
diff changeset
   266
            new Completion_Popup(Some(range), layered, loc2, font, items)
55978
56645c447ee9 tuned description and its rendering;
wenzelm
parents: 55914
diff changeset
   267
            {
55693
93ba0085e888 try explicit semantic completion before syntax completion;
wenzelm
parents: 55692
diff changeset
   268
              override def complete(item: Completion.Item) {
93ba0085e888 try explicit semantic completion before syntax completion;
wenzelm
parents: 55692
diff changeset
   269
                PIDE.completion_history.update(item)
93ba0085e888 try explicit semantic completion before syntax completion;
wenzelm
parents: 55692
diff changeset
   270
                insert(item)
93ba0085e888 try explicit semantic completion before syntax completion;
wenzelm
parents: 55692
diff changeset
   271
              }
93ba0085e888 try explicit semantic completion before syntax completion;
wenzelm
parents: 55692
diff changeset
   272
              override def propagate(evt: KeyEvent) {
56840
879fe16bd27c propagate more events, notably after hide_popup (e.g. LEFT, RIGHT);
wenzelm
parents: 56662
diff changeset
   273
                if (view.getKeyEventInterceptor == null)
879fe16bd27c propagate more events, notably after hide_popup (e.g. LEFT, RIGHT);
wenzelm
parents: 56662
diff changeset
   274
                  JEdit_Lib.propagate_key(view, evt)
879fe16bd27c propagate more events, notably after hide_popup (e.g. LEFT, RIGHT);
wenzelm
parents: 56662
diff changeset
   275
                else if (view.getKeyEventInterceptor == inner_key_listener) {
56197
416f7a00e4cb back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups;
wenzelm
parents: 56177
diff changeset
   276
                  try {
416f7a00e4cb back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups;
wenzelm
parents: 56177
diff changeset
   277
                    view.setKeyEventInterceptor(null)
416f7a00e4cb back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups;
wenzelm
parents: 56177
diff changeset
   278
                    JEdit_Lib.propagate_key(view, evt)
416f7a00e4cb back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups;
wenzelm
parents: 56177
diff changeset
   279
                  }
416f7a00e4cb back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups;
wenzelm
parents: 56177
diff changeset
   280
                  finally {
416f7a00e4cb back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups;
wenzelm
parents: 56177
diff changeset
   281
                    if (isDisplayable) view.setKeyEventInterceptor(inner_key_listener)
416f7a00e4cb back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups;
wenzelm
parents: 56177
diff changeset
   282
                  }
416f7a00e4cb back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups;
wenzelm
parents: 56177
diff changeset
   283
                }
56171
15351577da10 clarified key event propagation, in accordance to outer_key_listener;
wenzelm
parents: 56170
diff changeset
   284
                if (evt.getID == KeyEvent.KEY_TYPED) input(evt)
55693
93ba0085e888 try explicit semantic completion before syntax completion;
wenzelm
parents: 55692
diff changeset
   285
              }
56197
416f7a00e4cb back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups;
wenzelm
parents: 56177
diff changeset
   286
              override def shutdown(focus: Boolean) {
416f7a00e4cb back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups;
wenzelm
parents: 56177
diff changeset
   287
                if (view.getKeyEventInterceptor == inner_key_listener)
416f7a00e4cb back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups;
wenzelm
parents: 56177
diff changeset
   288
                  view.setKeyEventInterceptor(null)
416f7a00e4cb back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups;
wenzelm
parents: 56177
diff changeset
   289
                if (focus) text_area.requestFocus
56606
68b7a6db4a32 avoid ooddity: invoke intended function instead of java.awt.Container.invalidate();
wenzelm
parents: 56605
diff changeset
   290
                JEdit_Lib.invalidate_range(text_area, range)
56197
416f7a00e4cb back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups;
wenzelm
parents: 56177
diff changeset
   291
              }
55693
93ba0085e888 try explicit semantic completion before syntax completion;
wenzelm
parents: 55692
diff changeset
   292
            }
93ba0085e888 try explicit semantic completion before syntax completion;
wenzelm
parents: 55692
diff changeset
   293
          completion_popup = Some(completion)
56197
416f7a00e4cb back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups;
wenzelm
parents: 56177
diff changeset
   294
          view.setKeyEventInterceptor(completion.inner_key_listener)
56606
68b7a6db4a32 avoid ooddity: invoke intended function instead of java.awt.Container.invalidate();
wenzelm
parents: 56605
diff changeset
   295
          JEdit_Lib.invalidate_range(text_area, range)
56841
bc6faeadbf82 reduced cluttering of popups;
wenzelm
parents: 56840
diff changeset
   296
          Pretty_Tooltip.dismissed_all()
56197
416f7a00e4cb back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups;
wenzelm
parents: 56177
diff changeset
   297
          completion.show_popup(false)
55693
93ba0085e888 try explicit semantic completion before syntax completion;
wenzelm
parents: 55692
diff changeset
   298
        }
93ba0085e888 try explicit semantic completion before syntax completion;
wenzelm
parents: 55692
diff changeset
   299
      }
93ba0085e888 try explicit semantic completion before syntax completion;
wenzelm
parents: 55692
diff changeset
   300
56175
79c29244b377 merge semantic and syntax completion;
wenzelm
parents: 56173
diff changeset
   301
      if (buffer.isEditable) {
79c29244b377 merge semantic and syntax completion;
wenzelm
parents: 56173
diff changeset
   302
        val (no_completion, semantic_completion, opt_rendering) =
79c29244b377 merge semantic and syntax completion;
wenzelm
parents: 56173
diff changeset
   303
        {
79c29244b377 merge semantic and syntax completion;
wenzelm
parents: 56173
diff changeset
   304
          PIDE.document_view(text_area) match {
79c29244b377 merge semantic and syntax completion;
wenzelm
parents: 56173
diff changeset
   305
            case Some(doc_view) =>
79c29244b377 merge semantic and syntax completion;
wenzelm
parents: 56173
diff changeset
   306
              val rendering = doc_view.get_rendering()
79c29244b377 merge semantic and syntax completion;
wenzelm
parents: 56173
diff changeset
   307
              val (no_completion, result) =
56593
0ea7c84110ac back to unrestricted before_caret_range, which is important for quick editing at the end of line (amending 83777a91f5de);
wenzelm
parents: 56589
diff changeset
   308
              {
0ea7c84110ac back to unrestricted before_caret_range, which is important for quick editing at the end of line (amending 83777a91f5de);
wenzelm
parents: 56589
diff changeset
   309
                val caret_range = JEdit_Lib.before_caret_range(text_area, rendering)
0ea7c84110ac back to unrestricted before_caret_range, which is important for quick editing at the end of line (amending 83777a91f5de);
wenzelm
parents: 56589
diff changeset
   310
                rendering.semantic_completion(caret_range) match {
0ea7c84110ac back to unrestricted before_caret_range, which is important for quick editing at the end of line (amending 83777a91f5de);
wenzelm
parents: 56589
diff changeset
   311
                  case Some(Text.Info(_, Completion.No_Completion)) => (true, None)
0ea7c84110ac back to unrestricted before_caret_range, which is important for quick editing at the end of line (amending 83777a91f5de);
wenzelm
parents: 56589
diff changeset
   312
                  case Some(Text.Info(range, names: Completion.Names)) =>
0ea7c84110ac back to unrestricted before_caret_range, which is important for quick editing at the end of line (amending 83777a91f5de);
wenzelm
parents: 56589
diff changeset
   313
                    val result =
0ea7c84110ac back to unrestricted before_caret_range, which is important for quick editing at the end of line (amending 83777a91f5de);
wenzelm
parents: 56589
diff changeset
   314
                      JEdit_Lib.try_get_text(buffer, range) match {
0ea7c84110ac back to unrestricted before_caret_range, which is important for quick editing at the end of line (amending 83777a91f5de);
wenzelm
parents: 56589
diff changeset
   315
                        case Some(original) => names.complete(range, history, decode, original)
0ea7c84110ac back to unrestricted before_caret_range, which is important for quick editing at the end of line (amending 83777a91f5de);
wenzelm
parents: 56589
diff changeset
   316
                        case None => None
0ea7c84110ac back to unrestricted before_caret_range, which is important for quick editing at the end of line (amending 83777a91f5de);
wenzelm
parents: 56589
diff changeset
   317
                      }
0ea7c84110ac back to unrestricted before_caret_range, which is important for quick editing at the end of line (amending 83777a91f5de);
wenzelm
parents: 56589
diff changeset
   318
                    (false, result)
56587
83777a91f5de clarified before_caret_range: prevent continuation on next line;
wenzelm
parents: 56586
diff changeset
   319
                  case None => (false, None)
56175
79c29244b377 merge semantic and syntax completion;
wenzelm
parents: 56173
diff changeset
   320
                }
56593
0ea7c84110ac back to unrestricted before_caret_range, which is important for quick editing at the end of line (amending 83777a91f5de);
wenzelm
parents: 56589
diff changeset
   321
              }
56175
79c29244b377 merge semantic and syntax completion;
wenzelm
parents: 56173
diff changeset
   322
              (no_completion, result, Some(rendering))
56587
83777a91f5de clarified before_caret_range: prevent continuation on next line;
wenzelm
parents: 56586
diff changeset
   323
            case None => (false, None, None)
56175
79c29244b377 merge semantic and syntax completion;
wenzelm
parents: 56173
diff changeset
   324
          }
55693
93ba0085e888 try explicit semantic completion before syntax completion;
wenzelm
parents: 55692
diff changeset
   325
        }
56326
c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549;
wenzelm
parents: 56325
diff changeset
   326
        if (no_completion) false
c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549;
wenzelm
parents: 56325
diff changeset
   327
        else {
56564
94c55cc73747 added spell-checker completion dialog, without counting frequency of items due to empty name;
wenzelm
parents: 56326
diff changeset
   328
          val result =
56586
5ef60881681d explicit menu action to complete word;
wenzelm
parents: 56576
diff changeset
   329
          {
5ef60881681d explicit menu action to complete word;
wenzelm
parents: 56576
diff changeset
   330
            val result0 =
5ef60881681d explicit menu action to complete word;
wenzelm
parents: 56576
diff changeset
   331
              if (word_only) None
5ef60881681d explicit menu action to complete word;
wenzelm
parents: 56576
diff changeset
   332
              else
56587
83777a91f5de clarified before_caret_range: prevent continuation on next line;
wenzelm
parents: 56586
diff changeset
   333
                Completion.Result.merge(history, semantic_completion,
83777a91f5de clarified before_caret_range: prevent continuation on next line;
wenzelm
parents: 56586
diff changeset
   334
                  syntax_completion(history, explicit, opt_rendering))
56564
94c55cc73747 added spell-checker completion dialog, without counting frequency of items due to empty name;
wenzelm
parents: 56326
diff changeset
   335
            opt_rendering match {
94c55cc73747 added spell-checker completion dialog, without counting frequency of items due to empty name;
wenzelm
parents: 56326
diff changeset
   336
              case None => result0
94c55cc73747 added spell-checker completion dialog, without counting frequency of items due to empty name;
wenzelm
parents: 56326
diff changeset
   337
              case Some(rendering) =>
94c55cc73747 added spell-checker completion dialog, without counting frequency of items due to empty name;
wenzelm
parents: 56326
diff changeset
   338
                Completion.Result.merge(history, result0, spell_checker_completion(rendering))
94c55cc73747 added spell-checker completion dialog, without counting frequency of items due to empty name;
wenzelm
parents: 56326
diff changeset
   339
            }
56586
5ef60881681d explicit menu action to complete word;
wenzelm
parents: 56576
diff changeset
   340
          }
56175
79c29244b377 merge semantic and syntax completion;
wenzelm
parents: 56173
diff changeset
   341
          result match {
79c29244b377 merge semantic and syntax completion;
wenzelm
parents: 56173
diff changeset
   342
            case Some(result) =>
79c29244b377 merge semantic and syntax completion;
wenzelm
parents: 56173
diff changeset
   343
              result.items match {
79c29244b377 merge semantic and syntax completion;
wenzelm
parents: 56173
diff changeset
   344
                case List(item) if result.unique && item.immediate && immediate =>
79c29244b377 merge semantic and syntax completion;
wenzelm
parents: 56173
diff changeset
   345
                  insert(item)
56326
c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549;
wenzelm
parents: 56325
diff changeset
   346
                  true
c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549;
wenzelm
parents: 56325
diff changeset
   347
                case _ :: _ if !delayed =>
56175
79c29244b377 merge semantic and syntax completion;
wenzelm
parents: 56173
diff changeset
   348
                  open_popup(result)
56326
c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549;
wenzelm
parents: 56325
diff changeset
   349
                  false
c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549;
wenzelm
parents: 56325
diff changeset
   350
                case _ => false
56175
79c29244b377 merge semantic and syntax completion;
wenzelm
parents: 56173
diff changeset
   351
              }
56326
c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549;
wenzelm
parents: 56325
diff changeset
   352
            case None => false
56175
79c29244b377 merge semantic and syntax completion;
wenzelm
parents: 56173
diff changeset
   353
          }
53292
f567c1c7b180 option to insert unique completion immediately into buffer;
wenzelm
parents: 53275
diff changeset
   354
        }
55752
43d0e2a34c9d uniform insert vs. popup policy;
wenzelm
parents: 55749
diff changeset
   355
      }
56326
c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549;
wenzelm
parents: 56325
diff changeset
   356
      else false
53292
f567c1c7b180 option to insert unique completion immediately into buffer;
wenzelm
parents: 53275
diff changeset
   357
    }
f567c1c7b180 option to insert unique completion immediately into buffer;
wenzelm
parents: 53275
diff changeset
   358
f567c1c7b180 option to insert unique completion immediately into buffer;
wenzelm
parents: 53275
diff changeset
   359
f567c1c7b180 option to insert unique completion immediately into buffer;
wenzelm
parents: 53275
diff changeset
   360
    /* input key events */
53273
473ea1ed7503 some completion options;
wenzelm
parents: 53272
diff changeset
   361
53272
0dfd78ff7696 more abstract Completion_Popup.Text_Area;
wenzelm
parents: 53247
diff changeset
   362
    def input(evt: KeyEvent)
53242
142f4fff4e40 tuned signature;
wenzelm
parents: 53237
diff changeset
   363
    {
56662
f373fb77e0a4 avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
wenzelm
parents: 56606
diff changeset
   364
      Swing_Thread.require {}
53233
4b422e5d64fd some actual completion via outer syntax;
wenzelm
parents: 53232
diff changeset
   365
53273
473ea1ed7503 some completion options;
wenzelm
parents: 53272
diff changeset
   366
      if (PIDE.options.bool("jedit_completion")) {
473ea1ed7503 some completion options;
wenzelm
parents: 53272
diff changeset
   367
        if (!evt.isConsumed) {
473ea1ed7503 some completion options;
wenzelm
parents: 53272
diff changeset
   368
          dismissed()
53397
b179cdfa9d82 no completion on backspace -- too intrusive, e.g. when deleting keywords;
wenzelm
parents: 53337
diff changeset
   369
          if (evt.getKeyChar != '\b') {
53784
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   370
            val special = JEdit_Lib.special_key(evt)
56326
c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549;
wenzelm
parents: 56325
diff changeset
   371
            val immediate = PIDE.options.bool("jedit_completion_immediate")
53397
b179cdfa9d82 no completion on backspace -- too intrusive, e.g. when deleting keywords;
wenzelm
parents: 53337
diff changeset
   372
            if (PIDE.options.seconds("jedit_completion_delay").is_zero && !special) {
b179cdfa9d82 no completion on backspace -- too intrusive, e.g. when deleting keywords;
wenzelm
parents: 53337
diff changeset
   373
              input_delay.revoke()
56326
c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549;
wenzelm
parents: 56325
diff changeset
   374
              action(immediate = immediate)
53397
b179cdfa9d82 no completion on backspace -- too intrusive, e.g. when deleting keywords;
wenzelm
parents: 53337
diff changeset
   375
            }
56326
c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549;
wenzelm
parents: 56325
diff changeset
   376
            else {
c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549;
wenzelm
parents: 56325
diff changeset
   377
              if (!special && action(immediate = immediate, delayed = true))
c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549;
wenzelm
parents: 56325
diff changeset
   378
                input_delay.revoke()
c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549;
wenzelm
parents: 56325
diff changeset
   379
              else
c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549;
wenzelm
parents: 56325
diff changeset
   380
                input_delay.invoke()
c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549;
wenzelm
parents: 56325
diff changeset
   381
            }
53292
f567c1c7b180 option to insert unique completion immediately into buffer;
wenzelm
parents: 53275
diff changeset
   382
          }
53242
142f4fff4e40 tuned signature;
wenzelm
parents: 53237
diff changeset
   383
        }
53228
f6c6688961db some key event handling in the manner of SideKickBindings, SideKickCompletionPopup;
wenzelm
parents: 53226
diff changeset
   384
      }
f6c6688961db some key event handling in the manner of SideKickBindings, SideKickCompletionPopup;
wenzelm
parents: 53226
diff changeset
   385
    }
53273
473ea1ed7503 some completion options;
wenzelm
parents: 53272
diff changeset
   386
473ea1ed7503 some completion options;
wenzelm
parents: 53272
diff changeset
   387
    private val input_delay =
53292
f567c1c7b180 option to insert unique completion immediately into buffer;
wenzelm
parents: 53275
diff changeset
   388
      Swing_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay")) {
53322
a4cd032172e0 allow short words for explicit completion;
wenzelm
parents: 53297
diff changeset
   389
        action()
53292
f567c1c7b180 option to insert unique completion immediately into buffer;
wenzelm
parents: 53275
diff changeset
   390
      }
53273
473ea1ed7503 some completion options;
wenzelm
parents: 53272
diff changeset
   391
473ea1ed7503 some completion options;
wenzelm
parents: 53272
diff changeset
   392
53292
f567c1c7b180 option to insert unique completion immediately into buffer;
wenzelm
parents: 53275
diff changeset
   393
    /* dismiss popup */
53273
473ea1ed7503 some completion options;
wenzelm
parents: 53272
diff changeset
   394
53292
f567c1c7b180 option to insert unique completion immediately into buffer;
wenzelm
parents: 53275
diff changeset
   395
    def dismissed(): Boolean =
f567c1c7b180 option to insert unique completion immediately into buffer;
wenzelm
parents: 53275
diff changeset
   396
    {
56662
f373fb77e0a4 avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
wenzelm
parents: 56606
diff changeset
   397
      Swing_Thread.require {}
53273
473ea1ed7503 some completion options;
wenzelm
parents: 53272
diff changeset
   398
53292
f567c1c7b180 option to insert unique completion immediately into buffer;
wenzelm
parents: 53275
diff changeset
   399
      completion_popup match {
f567c1c7b180 option to insert unique completion immediately into buffer;
wenzelm
parents: 53275
diff changeset
   400
        case Some(completion) =>
f567c1c7b180 option to insert unique completion immediately into buffer;
wenzelm
parents: 53275
diff changeset
   401
          completion.hide_popup()
f567c1c7b180 option to insert unique completion immediately into buffer;
wenzelm
parents: 53275
diff changeset
   402
          completion_popup = None
f567c1c7b180 option to insert unique completion immediately into buffer;
wenzelm
parents: 53275
diff changeset
   403
          true
f567c1c7b180 option to insert unique completion immediately into buffer;
wenzelm
parents: 53275
diff changeset
   404
        case None =>
f567c1c7b180 option to insert unique completion immediately into buffer;
wenzelm
parents: 53275
diff changeset
   405
          false
53273
473ea1ed7503 some completion options;
wenzelm
parents: 53272
diff changeset
   406
      }
53292
f567c1c7b180 option to insert unique completion immediately into buffer;
wenzelm
parents: 53275
diff changeset
   407
    }
53274
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
   408
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
   409
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
   410
    /* activation */
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
   411
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
   412
    private val outer_key_listener =
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
   413
      JEdit_Lib.key_listener(key_typed = input _)
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
   414
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
   415
    private def activate()
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
   416
    {
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
   417
      text_area.addKeyListener(outer_key_listener)
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
   418
    }
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
   419
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
   420
    private def deactivate()
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
   421
    {
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
   422
      dismissed()
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
   423
      text_area.removeKeyListener(outer_key_listener)
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
   424
    }
53228
f6c6688961db some key event handling in the manner of SideKickBindings, SideKickCompletionPopup;
wenzelm
parents: 53226
diff changeset
   425
  }
53784
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   426
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   427
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   428
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   429
  /** history text field **/
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   430
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   431
  class History_Text_Field(
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   432
    name: String = null,
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   433
    instant_popups: Boolean = false,
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   434
    enter_adds_to_history: Boolean = true,
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   435
    syntax: Outer_Syntax = Outer_Syntax.init) extends
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   436
    HistoryTextField(name, instant_popups, enter_adds_to_history)
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   437
  {
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   438
    text_field =>
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   439
53848
8d7029eb0c31 disable standard behaviour of Mac OS X text field (i.e. select-all after focus gain) in order to make completion work more smoothly;
wenzelm
parents: 53784
diff changeset
   440
    // see https://forums.oracle.com/thread/1361677
8d7029eb0c31 disable standard behaviour of Mac OS X text field (i.e. select-all after focus gain) in order to make completion work more smoothly;
wenzelm
parents: 53784
diff changeset
   441
    if (GUI.is_macos_laf) text_field.setCaret(new DefaultCaret)
53784
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   442
55711
9e3d64e5919a paint completion range of active popup;
wenzelm
parents: 55693
diff changeset
   443
    // owned by Swing thread
53784
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   444
    private var completion_popup: Option[Completion_Popup] = None
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   445
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   446
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   447
    /* dismiss */
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   448
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   449
    private def dismissed(): Boolean =
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   450
    {
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   451
      completion_popup match {
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   452
        case Some(completion) =>
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   453
          completion.hide_popup()
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   454
          completion_popup = None
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   455
          true
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   456
        case None =>
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   457
          false
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   458
      }
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   459
    }
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   460
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   461
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   462
    /* insert */
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   463
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   464
    private def insert(item: Completion.Item)
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   465
    {
56662
f373fb77e0a4 avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
wenzelm
parents: 56606
diff changeset
   466
      Swing_Thread.require {}
53784
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   467
55692
19e8b00684f7 more explicit Completion.Item.range, independently of caret;
wenzelm
parents: 55690
diff changeset
   468
      val range = item.range
19e8b00684f7 more explicit Completion.Item.range, independently of caret;
wenzelm
parents: 55690
diff changeset
   469
      if (text_field.isEditable && range.length > 0) {
53784
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   470
        val content = text_field.getText
55692
19e8b00684f7 more explicit Completion.Item.range, independently of caret;
wenzelm
parents: 55690
diff changeset
   471
        JEdit_Lib.try_get_text(content, range) match {
53784
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   472
          case Some(text) if text == item.original =>
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   473
            text_field.setText(
55692
19e8b00684f7 more explicit Completion.Item.range, independently of caret;
wenzelm
parents: 55690
diff changeset
   474
              content.substring(0, range.start) +
53784
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   475
              item.replacement +
55692
19e8b00684f7 more explicit Completion.Item.range, independently of caret;
wenzelm
parents: 55690
diff changeset
   476
              content.substring(range.stop))
19e8b00684f7 more explicit Completion.Item.range, independently of caret;
wenzelm
parents: 55690
diff changeset
   477
            text_field.getCaret.setDot(range.start + item.replacement.length + item.move)
53784
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   478
          case _ =>
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   479
        }
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   480
      }
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   481
    }
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   482
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   483
56170
638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time;
wenzelm
parents: 55978
diff changeset
   484
    /* completion action: text field */
53784
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   485
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   486
    def action()
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   487
    {
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   488
      GUI.layered_pane(text_field) match {
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   489
        case Some(layered) if text_field.isEditable =>
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   490
          val history = PIDE.completion_history.value
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   491
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   492
          val caret = text_field.getCaret.getDot
55813
08a1c860bc12 allow completion within a word (or symbol), like semantic completion;
wenzelm
parents: 55767
diff changeset
   493
          val text = text_field.getText
55748
2e1398b484aa no word completion within word context;
wenzelm
parents: 55747
diff changeset
   494
55749
75a48dc4383e tuned signature;
wenzelm
parents: 55748
diff changeset
   495
          val context = syntax.language_context
55748
2e1398b484aa no word completion within word context;
wenzelm
parents: 55747
diff changeset
   496
55813
08a1c860bc12 allow completion within a word (or symbol), like semantic completion;
wenzelm
parents: 55767
diff changeset
   497
          syntax.completion.complete(history, true, false, 0, text, caret, false, context) match {
53784
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   498
            case Some(result) =>
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   499
              val fm = text_field.getFontMetrics(text_field.getFont)
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   500
              val loc =
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   501
                SwingUtilities.convertPoint(text_field, fm.stringWidth(text), fm.getHeight, layered)
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   502
55978
56645c447ee9 tuned description and its rendering;
wenzelm
parents: 55914
diff changeset
   503
              val items = result.items.map(new Item(_))
55711
9e3d64e5919a paint completion range of active popup;
wenzelm
parents: 55693
diff changeset
   504
              val completion =
55978
56645c447ee9 tuned description and its rendering;
wenzelm
parents: 55914
diff changeset
   505
                new Completion_Popup(None, layered, loc, text_field.getFont, items)
56645c447ee9 tuned description and its rendering;
wenzelm
parents: 55914
diff changeset
   506
                {
56645c447ee9 tuned description and its rendering;
wenzelm
parents: 55914
diff changeset
   507
                  override def complete(item: Completion.Item) {
56645c447ee9 tuned description and its rendering;
wenzelm
parents: 55914
diff changeset
   508
                    PIDE.completion_history.update(item)
56645c447ee9 tuned description and its rendering;
wenzelm
parents: 55914
diff changeset
   509
                    insert(item)
56645c447ee9 tuned description and its rendering;
wenzelm
parents: 55914
diff changeset
   510
                  }
56645c447ee9 tuned description and its rendering;
wenzelm
parents: 55914
diff changeset
   511
                  override def propagate(evt: KeyEvent) {
56645c447ee9 tuned description and its rendering;
wenzelm
parents: 55914
diff changeset
   512
                    if (!evt.isConsumed) text_field.processKeyEvent(evt)
56645c447ee9 tuned description and its rendering;
wenzelm
parents: 55914
diff changeset
   513
                  }
56197
416f7a00e4cb back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups;
wenzelm
parents: 56177
diff changeset
   514
                  override def shutdown(focus: Boolean) { if (focus) text_field.requestFocus }
53784
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   515
                }
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   516
              completion_popup = Some(completion)
56197
416f7a00e4cb back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups;
wenzelm
parents: 56177
diff changeset
   517
              completion.show_popup(true)
53784
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   518
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   519
            case None =>
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   520
          }
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   521
        case _ =>
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   522
      }
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   523
    }
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   524
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   525
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   526
    /* process key event */
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   527
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   528
    private def process(evt: KeyEvent)
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   529
    {
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   530
      if (PIDE.options.bool("jedit_completion")) {
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   531
        dismissed()
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   532
        if (evt.getKeyChar != '\b') {
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   533
          val special = JEdit_Lib.special_key(evt)
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   534
          if (PIDE.options.seconds("jedit_completion_delay").is_zero && !special) {
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   535
            process_delay.revoke()
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   536
            action()
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   537
          }
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   538
          else process_delay.invoke()
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   539
        }
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   540
      }
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   541
    }
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   542
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   543
    private val process_delay =
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   544
      Swing_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay")) {
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   545
        action()
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   546
      }
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   547
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   548
    override def processKeyEvent(evt0: KeyEvent)
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   549
    {
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   550
      val evt = KeyEventWorkaround.processKeyEvent(evt0)
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   551
      if (evt != null) {
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   552
        evt.getID match {
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   553
          case KeyEvent.KEY_PRESSED =>
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   554
            val key_code = evt.getKeyCode
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   555
            if (key_code == KeyEvent.VK_ESCAPE) {
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   556
              if (dismissed()) evt.consume
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   557
            }
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   558
          case KeyEvent.KEY_TYPED =>
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   559
            super.processKeyEvent(evt)
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   560
            process(evt)
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   561
            evt.consume
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   562
          case _ =>
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   563
        }
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   564
        if (!evt.isConsumed) super.processKeyEvent(evt)
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   565
      }
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   566
    }
322a3ff42b33 completion popup for history text field;
wenzelm
parents: 53407
diff changeset
   567
  }
53023
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   568
}
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   569
53233
4b422e5d64fd some actual completion via outer syntax;
wenzelm
parents: 53232
diff changeset
   570
53023
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   571
class Completion_Popup private(
56605
wenzelm
parents: 56593
diff changeset
   572
  opt_range: Option[Text.Range],
53246
8d34caf5bf82 more elementary Popup via JLayeredPane -- avoid javax.swing.PopupFactory with its many problems and dangers of accidental HeavyWeightPopup (especially on Mac OS X);
wenzelm
parents: 53244
diff changeset
   573
  layered: JLayeredPane,
8d34caf5bf82 more elementary Popup via JLayeredPane -- avoid javax.swing.PopupFactory with its many problems and dangers of accidental HeavyWeightPopup (especially on Mac OS X);
wenzelm
parents: 53244
diff changeset
   574
  location: Point,
53272
0dfd78ff7696 more abstract Completion_Popup.Text_Area;
wenzelm
parents: 53247
diff changeset
   575
  font: Font,
55978
56645c447ee9 tuned description and its rendering;
wenzelm
parents: 55914
diff changeset
   576
  items: List[Completion_Popup.Item]) extends JPanel(new BorderLayout)
53023
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   577
{
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   578
  completion =>
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   579
56662
f373fb77e0a4 avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
wenzelm
parents: 56606
diff changeset
   580
  Swing_Thread.require {}
53405
ed2b48af04d9 interpret keys more movement only when needed;
wenzelm
parents: 53398
diff changeset
   581
53232
4a3762693452 tuned signature;
wenzelm
parents: 53231
diff changeset
   582
  require(!items.isEmpty)
53405
ed2b48af04d9 interpret keys more movement only when needed;
wenzelm
parents: 53398
diff changeset
   583
  val multi = items.length > 1
53232
4a3762693452 tuned signature;
wenzelm
parents: 53231
diff changeset
   584
4a3762693452 tuned signature;
wenzelm
parents: 53231
diff changeset
   585
4a3762693452 tuned signature;
wenzelm
parents: 53231
diff changeset
   586
  /* actions */
4a3762693452 tuned signature;
wenzelm
parents: 53231
diff changeset
   587
53275
b34aac6511ab tuned signature;
wenzelm
parents: 53274
diff changeset
   588
  def complete(item: Completion.Item) { }
53232
4a3762693452 tuned signature;
wenzelm
parents: 53231
diff changeset
   589
  def propagate(evt: KeyEvent) { }
56197
416f7a00e4cb back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups;
wenzelm
parents: 56177
diff changeset
   590
  def shutdown(focus: Boolean) { }
53023
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   591
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   592
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   593
  /* list view */
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   594
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   595
  private val list_view = new ListView(items)
53272
0dfd78ff7696 more abstract Completion_Popup.Text_Area;
wenzelm
parents: 53247
diff changeset
   596
  list_view.font = font
53023
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   597
  list_view.selection.intervalMode = ListView.IntervalMode.Single
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   598
  list_view.peer.setFocusTraversalKeysEnabled(false)
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   599
  list_view.peer.setVisibleRowCount(items.length min 8)
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   600
  list_view.peer.setSelectedIndex(0)
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   601
53398
f8b150e8778b remove Swing input map, which might bind keys in unexpected ways (e.g. LEFT/RIGHT in singleton list);
wenzelm
parents: 53397
diff changeset
   602
  for (cond <-
f8b150e8778b remove Swing input map, which might bind keys in unexpected ways (e.g. LEFT/RIGHT in singleton list);
wenzelm
parents: 53397
diff changeset
   603
    List(JComponent.WHEN_FOCUSED,
f8b150e8778b remove Swing input map, which might bind keys in unexpected ways (e.g. LEFT/RIGHT in singleton list);
wenzelm
parents: 53397
diff changeset
   604
      JComponent.WHEN_ANCESTOR_OF_FOCUSED_COMPONENT,
f8b150e8778b remove Swing input map, which might bind keys in unexpected ways (e.g. LEFT/RIGHT in singleton list);
wenzelm
parents: 53397
diff changeset
   605
      JComponent.WHEN_IN_FOCUSED_WINDOW)) list_view.peer.setInputMap(cond, null)
f8b150e8778b remove Swing input map, which might bind keys in unexpected ways (e.g. LEFT/RIGHT in singleton list);
wenzelm
parents: 53397
diff changeset
   606
53023
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   607
  private def complete_selected(): Boolean =
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   608
  {
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   609
    list_view.selection.items.toList match {
55978
56645c447ee9 tuned description and its rendering;
wenzelm
parents: 55914
diff changeset
   610
      case item :: _ => complete(item.item); true
53023
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   611
      case _ => false
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   612
    }
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   613
  }
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   614
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   615
  private def move_items(n: Int)
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   616
  {
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   617
    val i = list_view.peer.getSelectedIndex
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   618
    val j = ((i + n) min (items.length - 1)) max 0
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   619
    if (i != j) {
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   620
      list_view.peer.setSelectedIndex(j)
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   621
      list_view.peer.ensureIndexIsVisible(j)
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   622
    }
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   623
  }
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   624
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   625
  private def move_pages(n: Int)
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   626
  {
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   627
    val page_size = list_view.peer.getVisibleRowCount - 1
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   628
    move_items(page_size * n)
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   629
  }
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   630
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   631
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   632
  /* event handling */
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   633
56197
416f7a00e4cb back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups;
wenzelm
parents: 56177
diff changeset
   634
  val inner_key_listener =
53226
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53023
diff changeset
   635
    JEdit_Lib.key_listener(
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53023
diff changeset
   636
      key_pressed = (e: KeyEvent) =>
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53023
diff changeset
   637
        {
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53023
diff changeset
   638
          if (!e.isConsumed) {
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53023
diff changeset
   639
            e.getKeyCode match {
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53023
diff changeset
   640
              case KeyEvent.VK_TAB =>
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53023
diff changeset
   641
                if (complete_selected()) e.consume
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53023
diff changeset
   642
                hide_popup()
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53023
diff changeset
   643
              case KeyEvent.VK_ESCAPE =>
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53023
diff changeset
   644
                hide_popup()
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53023
diff changeset
   645
                e.consume
53405
ed2b48af04d9 interpret keys more movement only when needed;
wenzelm
parents: 53398
diff changeset
   646
              case KeyEvent.VK_UP | KeyEvent.VK_KP_UP if multi =>
53407
wenzelm
parents: 53405
diff changeset
   647
                move_items(-1)
wenzelm
parents: 53405
diff changeset
   648
                e.consume
53405
ed2b48af04d9 interpret keys more movement only when needed;
wenzelm
parents: 53398
diff changeset
   649
              case KeyEvent.VK_DOWN | KeyEvent.VK_KP_DOWN if multi =>
53407
wenzelm
parents: 53405
diff changeset
   650
                move_items(1)
wenzelm
parents: 53405
diff changeset
   651
                e.consume
53405
ed2b48af04d9 interpret keys more movement only when needed;
wenzelm
parents: 53398
diff changeset
   652
              case KeyEvent.VK_PAGE_UP if multi =>
53407
wenzelm
parents: 53405
diff changeset
   653
                move_pages(-1)
wenzelm
parents: 53405
diff changeset
   654
                e.consume
53405
ed2b48af04d9 interpret keys more movement only when needed;
wenzelm
parents: 53398
diff changeset
   655
              case KeyEvent.VK_PAGE_DOWN if multi =>
53407
wenzelm
parents: 53405
diff changeset
   656
                move_pages(1)
wenzelm
parents: 53405
diff changeset
   657
                e.consume
53226
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53023
diff changeset
   658
              case _ =>
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53023
diff changeset
   659
                if (e.isActionKey || e.isAltDown || e.isMetaDown || e.isControlDown)
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53023
diff changeset
   660
                  hide_popup()
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53023
diff changeset
   661
            }
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53023
diff changeset
   662
          }
53232
4a3762693452 tuned signature;
wenzelm
parents: 53231
diff changeset
   663
          propagate(e)
53226
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53023
diff changeset
   664
        },
53232
4a3762693452 tuned signature;
wenzelm
parents: 53231
diff changeset
   665
      key_typed = propagate _
53226
9cf8e2263ca7 more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents: 53023
diff changeset
   666
    )
53023
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   667
53274
1760c01f1c78 maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents: 53273
diff changeset
   668
  list_view.peer.addKeyListener(inner_key_listener)
53023
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   669
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   670
  list_view.peer.addMouseListener(new MouseAdapter {
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   671
    override def mouseClicked(e: MouseEvent) {
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   672
      if (complete_selected()) e.consume
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   673
      hide_popup()
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   674
    }
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   675
  })
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   676
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   677
  list_view.peer.addFocusListener(new FocusAdapter {
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   678
    override def focusLost(e: FocusEvent) { hide_popup() }
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   679
  })
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   680
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   681
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   682
  /* main content */
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   683
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   684
  override def getFocusTraversalKeysEnabled = false
53297
64c31de7f21c border as for Pretty_Tooltip;
wenzelm
parents: 53296
diff changeset
   685
  completion.setBorder(new LineBorder(Color.BLACK))
53023
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   686
  completion.add((new ScrollPane(list_view)).peer.asInstanceOf[JComponent])
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   687
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   688
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   689
  /* popup */
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   690
56605
wenzelm
parents: 56593
diff changeset
   691
  def active_range: Option[Text.Range] =
wenzelm
parents: 56593
diff changeset
   692
    if (isDisplayable) opt_range else None
wenzelm
parents: 56593
diff changeset
   693
53023
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   694
  private val popup =
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   695
  {
53247
bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents: 53246
diff changeset
   696
    val screen = JEdit_Lib.screen_location(layered, location)
bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents: 53246
diff changeset
   697
    val size =
53230
6589ff56cc3c determine completion geometry like tooltip;
wenzelm
parents: 53229
diff changeset
   698
    {
6589ff56cc3c determine completion geometry like tooltip;
wenzelm
parents: 53229
diff changeset
   699
      val geometry = JEdit_Lib.window_geometry(completion, completion)
6589ff56cc3c determine completion geometry like tooltip;
wenzelm
parents: 53229
diff changeset
   700
      val bounds = Rendering.popup_bounds
53247
bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents: 53246
diff changeset
   701
      val w = geometry.width min (screen.bounds.width * bounds).toInt min layered.getWidth
bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents: 53246
diff changeset
   702
      val h = geometry.height min (screen.bounds.height * bounds).toInt min layered.getHeight
bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents: 53246
diff changeset
   703
      new Dimension(w, h)
53230
6589ff56cc3c determine completion geometry like tooltip;
wenzelm
parents: 53229
diff changeset
   704
    }
53247
bd595338ca18 uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents: 53246
diff changeset
   705
    new Popup(layered, completion, screen.relative(layered, size), size)
53246
8d34caf5bf82 more elementary Popup via JLayeredPane -- avoid javax.swing.PopupFactory with its many problems and dangers of accidental HeavyWeightPopup (especially on Mac OS X);
wenzelm
parents: 53244
diff changeset
   706
  }
8d34caf5bf82 more elementary Popup via JLayeredPane -- avoid javax.swing.PopupFactory with its many problems and dangers of accidental HeavyWeightPopup (especially on Mac OS X);
wenzelm
parents: 53244
diff changeset
   707
56197
416f7a00e4cb back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups;
wenzelm
parents: 56177
diff changeset
   708
  private def show_popup(focus: Boolean)
53246
8d34caf5bf82 more elementary Popup via JLayeredPane -- avoid javax.swing.PopupFactory with its many problems and dangers of accidental HeavyWeightPopup (especially on Mac OS X);
wenzelm
parents: 53244
diff changeset
   709
  {
8d34caf5bf82 more elementary Popup via JLayeredPane -- avoid javax.swing.PopupFactory with its many problems and dangers of accidental HeavyWeightPopup (especially on Mac OS X);
wenzelm
parents: 53244
diff changeset
   710
    popup.show
56197
416f7a00e4cb back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups;
wenzelm
parents: 56177
diff changeset
   711
    if (focus) list_view.requestFocus
53023
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   712
  }
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   713
53232
4a3762693452 tuned signature;
wenzelm
parents: 53231
diff changeset
   714
  private def hide_popup()
53023
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   715
  {
56197
416f7a00e4cb back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups;
wenzelm
parents: 56177
diff changeset
   716
    shutdown(list_view.peer.isFocusOwner)
416f7a00e4cb back to KeyEventInterceptor (see 423e29f1f304), but without focus change, which helps to avoid loosing key events due to quick opening and closing of popups;
wenzelm
parents: 56177
diff changeset
   717
    popup.hide
53023
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   718
  }
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   719
}
f127e949389f Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff changeset
   720