author | wenzelm |
Wed, 04 Sep 2013 12:20:00 +0200 | |
changeset 53398 | f8b150e8778b |
parent 53397 | b179cdfa9d82 |
child 53405 | ed2b48af04d9 |
permissions | -rw-r--r-- |
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 | 12 |
import java.awt.{Color, Font, Point, BorderLayout, Dimension} |
53296
65c60c782da5
less aggressive immediate completion, based on input and text;
wenzelm
parents:
53293
diff
changeset
|
13 |
import java.awt.event.{InputEvent, 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 | 15 |
import javax.swing.border.LineBorder |
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
|
16 |
|
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 |
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
|
18 |
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
|
19 |
|
53296
65c60c782da5
less aggressive immediate completion, based on input and text;
wenzelm
parents:
53293
diff
changeset
|
20 |
import org.gjt.sp.jedit.{View, Debug} |
53228
f6c6688961db
some key event handling in the manner of SideKickBindings, SideKickCompletionPopup;
wenzelm
parents:
53226
diff
changeset
|
21 |
import org.gjt.sp.jedit.textarea.JEditTextArea |
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
|
22 |
|
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
|
23 |
|
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 |
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
|
25 |
{ |
53272 | 26 |
/* setup for 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
|
27 |
|
53242 | 28 |
object Text_Area |
53233 | 29 |
{ |
53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
30 |
private val key = new Object |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
31 |
|
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
32 |
def apply(text_area: JEditTextArea): Option[Completion_Popup.Text_Area] = |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
33 |
text_area.getClientProperty(key) match { |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
34 |
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
|
35 |
case _ => None |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
36 |
} |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
37 |
|
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
38 |
def exit(text_area: JEditTextArea) |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
39 |
{ |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
40 |
Swing_Thread.require() |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
41 |
apply(text_area) match { |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
42 |
case None => |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
43 |
case Some(text_area_completion) => |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
44 |
text_area_completion.deactivate() |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
45 |
text_area.putClientProperty(key, null) |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
46 |
} |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
47 |
} |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
48 |
|
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
49 |
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
|
50 |
{ |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
51 |
exit(text_area) |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
52 |
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
|
53 |
text_area.putClientProperty(key, text_area_completion) |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
54 |
text_area_completion.activate() |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
55 |
text_area_completion |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
56 |
} |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
57 |
|
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
58 |
def dismissed(text_area: JEditTextArea): Boolean = |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
59 |
{ |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
60 |
Swing_Thread.require() |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
61 |
apply(text_area) match { |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
62 |
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
|
63 |
case None => false |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
64 |
} |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
65 |
} |
53272 | 66 |
} |
67 |
||
53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
68 |
class Text_Area private(text_area: JEditTextArea) |
53272 | 69 |
{ |
70 |
private var completion_popup: Option[Completion_Popup] = None |
|
71 |
||
72 |
||
53292
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
73 |
/* completion action */ |
53273 | 74 |
|
53275 | 75 |
private def insert(item: Completion.Item) |
53242 | 76 |
{ |
77 |
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
|
78 |
|
53242 | 79 |
val buffer = text_area.getBuffer |
80 |
val len = item.original.length |
|
81 |
if (buffer.isEditable && len > 0) { |
|
82 |
JEdit_Lib.buffer_edit(buffer) { |
|
83 |
val caret = text_area.getCaretPosition |
|
84 |
JEdit_Lib.try_get_text(buffer, Text.Range(caret - len, caret)) match { |
|
85 |
case Some(text) if text == item.original => |
|
86 |
buffer.remove(caret - len, len) |
|
87 |
buffer.insert(caret - len, item.replacement) |
|
88 |
case _ => |
|
89 |
} |
|
53233 | 90 |
} |
91 |
} |
|
92 |
} |
|
53242 | 93 |
|
53322 | 94 |
def action(immediate: Boolean = false, explicit: Boolean = false) |
53292
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
95 |
{ |
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
96 |
val view = text_area.getView |
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
97 |
val layered = view.getLayeredPane |
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
98 |
val buffer = text_area.getBuffer |
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
99 |
val painter = text_area.getPainter |
53273 | 100 |
|
53292
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
101 |
if (buffer.isEditable) { |
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
102 |
Isabelle.mode_syntax(JEdit_Lib.buffer_mode(buffer)) match { |
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
103 |
case Some(syntax) => |
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
104 |
val caret = text_area.getCaretPosition |
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
105 |
val line = buffer.getLineOfOffset(caret) |
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
106 |
val start = buffer.getLineStartOffset(line) |
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
107 |
val text = buffer.getSegment(start, caret - start) |
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
108 |
|
53337
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
109 |
val history = PIDE.completion_history.value |
53322 | 110 |
val decode = Isabelle_Encoding.is_active(buffer) |
53337
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
111 |
syntax.completion.complete(history, decode, explicit, text) match { |
53325
ffabc0083786
more explicit indication of unique result (see also 45be26b98ca6, 3d654643cf56);
wenzelm
parents:
53322
diff
changeset
|
112 |
case Some(result) => |
ffabc0083786
more explicit indication of unique result (see also 45be26b98ca6, 3d654643cf56);
wenzelm
parents:
53322
diff
changeset
|
113 |
if (result.unique && result.items.head.immediate && immediate) |
ffabc0083786
more explicit indication of unique result (see also 45be26b98ca6, 3d654643cf56);
wenzelm
parents:
53322
diff
changeset
|
114 |
insert(result.items.head) |
ffabc0083786
more explicit indication of unique result (see also 45be26b98ca6, 3d654643cf56);
wenzelm
parents:
53322
diff
changeset
|
115 |
else { |
ffabc0083786
more explicit indication of unique result (see also 45be26b98ca6, 3d654643cf56);
wenzelm
parents:
53322
diff
changeset
|
116 |
val font = |
ffabc0083786
more explicit indication of unique result (see also 45be26b98ca6, 3d654643cf56);
wenzelm
parents:
53322
diff
changeset
|
117 |
painter.getFont.deriveFont(Rendering.font_size("jedit_popup_font_scale")) |
53292
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
118 |
|
53325
ffabc0083786
more explicit indication of unique result (see also 45be26b98ca6, 3d654643cf56);
wenzelm
parents:
53322
diff
changeset
|
119 |
val loc1 = text_area.offsetToXY(caret - result.original.length) |
ffabc0083786
more explicit indication of unique result (see also 45be26b98ca6, 3d654643cf56);
wenzelm
parents:
53322
diff
changeset
|
120 |
if (loc1 != null) { |
ffabc0083786
more explicit indication of unique result (see also 45be26b98ca6, 3d654643cf56);
wenzelm
parents:
53322
diff
changeset
|
121 |
val loc2 = |
ffabc0083786
more explicit indication of unique result (see also 45be26b98ca6, 3d654643cf56);
wenzelm
parents:
53322
diff
changeset
|
122 |
SwingUtilities.convertPoint(painter, |
ffabc0083786
more explicit indication of unique result (see also 45be26b98ca6, 3d654643cf56);
wenzelm
parents:
53322
diff
changeset
|
123 |
loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered) |
53292
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
124 |
|
53325
ffabc0083786
more explicit indication of unique result (see also 45be26b98ca6, 3d654643cf56);
wenzelm
parents:
53322
diff
changeset
|
125 |
val completion = |
ffabc0083786
more explicit indication of unique result (see also 45be26b98ca6, 3d654643cf56);
wenzelm
parents:
53322
diff
changeset
|
126 |
new Completion_Popup(layered, loc2, font, result.items) { |
53337
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
127 |
override def complete(item: Completion.Item) { |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
128 |
PIDE.completion_history.update(item) |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
129 |
insert(item) |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53325
diff
changeset
|
130 |
} |
53325
ffabc0083786
more explicit indication of unique result (see also 45be26b98ca6, 3d654643cf56);
wenzelm
parents:
53322
diff
changeset
|
131 |
override def propagate(evt: KeyEvent) { |
ffabc0083786
more explicit indication of unique result (see also 45be26b98ca6, 3d654643cf56);
wenzelm
parents:
53322
diff
changeset
|
132 |
JEdit_Lib.propagate_key(view, evt) |
ffabc0083786
more explicit indication of unique result (see also 45be26b98ca6, 3d654643cf56);
wenzelm
parents:
53322
diff
changeset
|
133 |
input(evt) |
ffabc0083786
more explicit indication of unique result (see also 45be26b98ca6, 3d654643cf56);
wenzelm
parents:
53322
diff
changeset
|
134 |
} |
ffabc0083786
more explicit indication of unique result (see also 45be26b98ca6, 3d654643cf56);
wenzelm
parents:
53322
diff
changeset
|
135 |
override def refocus() { text_area.requestFocus } |
53292
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
136 |
} |
53325
ffabc0083786
more explicit indication of unique result (see also 45be26b98ca6, 3d654643cf56);
wenzelm
parents:
53322
diff
changeset
|
137 |
completion_popup = Some(completion) |
ffabc0083786
more explicit indication of unique result (see also 45be26b98ca6, 3d654643cf56);
wenzelm
parents:
53322
diff
changeset
|
138 |
completion.show_popup() |
ffabc0083786
more explicit indication of unique result (see also 45be26b98ca6, 3d654643cf56);
wenzelm
parents:
53322
diff
changeset
|
139 |
} |
53292
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
140 |
} |
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
141 |
case None => |
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
142 |
} |
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
143 |
case None => |
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
144 |
} |
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
145 |
} |
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
146 |
} |
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
147 |
|
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
148 |
|
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
149 |
/* input key events */ |
53273 | 150 |
|
53272 | 151 |
def input(evt: KeyEvent) |
53242 | 152 |
{ |
153 |
Swing_Thread.require() |
|
53233 | 154 |
|
53273 | 155 |
if (PIDE.options.bool("jedit_completion")) { |
156 |
if (!evt.isConsumed) { |
|
157 |
dismissed() |
|
53397
b179cdfa9d82
no completion on backspace -- too intrusive, e.g. when deleting keywords;
wenzelm
parents:
53337
diff
changeset
|
158 |
if (evt.getKeyChar != '\b') { |
b179cdfa9d82
no completion on backspace -- too intrusive, e.g. when deleting keywords;
wenzelm
parents:
53337
diff
changeset
|
159 |
val mod = evt.getModifiers |
b179cdfa9d82
no completion on backspace -- too intrusive, e.g. when deleting keywords;
wenzelm
parents:
53337
diff
changeset
|
160 |
val special = |
b179cdfa9d82
no completion on backspace -- too intrusive, e.g. when deleting keywords;
wenzelm
parents:
53337
diff
changeset
|
161 |
// cf. 5.1.0/jEdit/org/gjt/sp/jedit/gui/KeyEventWorkaround.java |
b179cdfa9d82
no completion on backspace -- too intrusive, e.g. when deleting keywords;
wenzelm
parents:
53337
diff
changeset
|
162 |
(mod & InputEvent.CTRL_MASK) != 0 && (mod & InputEvent.ALT_MASK) == 0 || |
b179cdfa9d82
no completion on backspace -- too intrusive, e.g. when deleting keywords;
wenzelm
parents:
53337
diff
changeset
|
163 |
(mod & InputEvent.CTRL_MASK) == 0 && (mod & InputEvent.ALT_MASK) != 0 && |
b179cdfa9d82
no completion on backspace -- too intrusive, e.g. when deleting keywords;
wenzelm
parents:
53337
diff
changeset
|
164 |
!Debug.ALT_KEY_PRESSED_DISABLED || |
b179cdfa9d82
no completion on backspace -- too intrusive, e.g. when deleting keywords;
wenzelm
parents:
53337
diff
changeset
|
165 |
(mod & InputEvent.META_MASK) != 0 |
53296
65c60c782da5
less aggressive immediate completion, based on input and text;
wenzelm
parents:
53293
diff
changeset
|
166 |
|
53397
b179cdfa9d82
no completion on backspace -- too intrusive, e.g. when deleting keywords;
wenzelm
parents:
53337
diff
changeset
|
167 |
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
|
168 |
input_delay.revoke() |
b179cdfa9d82
no completion on backspace -- too intrusive, e.g. when deleting keywords;
wenzelm
parents:
53337
diff
changeset
|
169 |
action(immediate = PIDE.options.bool("jedit_completion_immediate")) |
b179cdfa9d82
no completion on backspace -- too intrusive, e.g. when deleting keywords;
wenzelm
parents:
53337
diff
changeset
|
170 |
} |
b179cdfa9d82
no completion on backspace -- too intrusive, e.g. when deleting keywords;
wenzelm
parents:
53337
diff
changeset
|
171 |
else input_delay.invoke() |
53292
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
172 |
} |
53242 | 173 |
} |
53228
f6c6688961db
some key event handling in the manner of SideKickBindings, SideKickCompletionPopup;
wenzelm
parents:
53226
diff
changeset
|
174 |
} |
f6c6688961db
some key event handling in the manner of SideKickBindings, SideKickCompletionPopup;
wenzelm
parents:
53226
diff
changeset
|
175 |
} |
53273 | 176 |
|
177 |
private val input_delay = |
|
53292
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
178 |
Swing_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay")) { |
53322 | 179 |
action() |
53292
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
180 |
} |
53273 | 181 |
|
182 |
||
53292
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
183 |
/* dismiss popup */ |
53273 | 184 |
|
53292
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
185 |
def dismissed(): Boolean = |
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
186 |
{ |
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
187 |
Swing_Thread.require() |
53273 | 188 |
|
53292
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
189 |
completion_popup match { |
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
190 |
case Some(completion) => |
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
191 |
completion.hide_popup() |
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
192 |
completion_popup = None |
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
193 |
true |
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
194 |
case None => |
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
195 |
false |
53273 | 196 |
} |
53292
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
197 |
} |
53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
198 |
|
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
199 |
|
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
200 |
/* activation */ |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
201 |
|
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
202 |
private val outer_key_listener = |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
203 |
JEdit_Lib.key_listener(key_typed = input _) |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
204 |
|
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
205 |
private def activate() |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
206 |
{ |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
207 |
text_area.addKeyListener(outer_key_listener) |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
208 |
} |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
209 |
|
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
210 |
private def deactivate() |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
211 |
{ |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
212 |
dismissed() |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
213 |
text_area.removeKeyListener(outer_key_listener) |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
214 |
} |
53228
f6c6688961db
some key event handling in the manner of SideKickBindings, SideKickCompletionPopup;
wenzelm
parents:
53226
diff
changeset
|
215 |
} |
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
|
216 |
} |
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
|
217 |
|
53233 | 218 |
|
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
|
219 |
class Completion_Popup private( |
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
|
220 |
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
|
221 |
location: Point, |
53272 | 222 |
font: Font, |
53275 | 223 |
items: List[Completion.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
|
224 |
{ |
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
|
225 |
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
|
226 |
|
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
|
227 |
Swing_Thread.require() |
53232 | 228 |
require(!items.isEmpty) |
229 |
||
230 |
||
231 |
/* actions */ |
|
232 |
||
53275 | 233 |
def complete(item: Completion.Item) { } |
53232 | 234 |
def propagate(evt: KeyEvent) { } |
53234
ea4abbbe1702
more careful refocus operation: do not reset focus if it was already lost (relevant when activating a different GUI component, for example);
wenzelm
parents:
53233
diff
changeset
|
235 |
def refocus() { } |
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
|
236 |
|
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
|
237 |
|
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
|
238 |
/* 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
|
239 |
|
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
|
240 |
private val list_view = new ListView(items) |
53272 | 241 |
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
|
242 |
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
|
243 |
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
|
244 |
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
|
245 |
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
|
246 |
|
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
|
247 |
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
|
248 |
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
|
249 |
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
|
250 |
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
|
251 |
|
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
|
252 |
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
|
253 |
{ |
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
|
254 |
list_view.selection.items.toList match { |
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
|
255 |
case item :: _ => complete(item); true |
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
|
256 |
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
|
257 |
} |
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
|
258 |
} |
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
|
259 |
|
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
|
260 |
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
|
261 |
{ |
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
|
262 |
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
|
263 |
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
|
264 |
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
|
265 |
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
|
266 |
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
|
267 |
} |
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
|
268 |
} |
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
|
269 |
|
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
|
270 |
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
|
271 |
{ |
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
|
272 |
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
|
273 |
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
|
274 |
} |
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
|
275 |
|
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
|
276 |
|
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
|
277 |
/* 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
|
278 |
|
53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
279 |
private val inner_key_listener = |
53226
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
280 |
JEdit_Lib.key_listener( |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
281 |
key_pressed = (e: KeyEvent) => |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
282 |
{ |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
283 |
if (!e.isConsumed) { |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
284 |
e.getKeyCode match { |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
285 |
case KeyEvent.VK_TAB => |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
286 |
if (complete_selected()) e.consume |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
287 |
hide_popup() |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
288 |
case KeyEvent.VK_ESCAPE => |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
289 |
hide_popup() |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
290 |
e.consume |
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
|
291 |
case KeyEvent.VK_UP | KeyEvent.VK_KP_UP => move_items(-1); e.consume |
f8b150e8778b
remove Swing input map, which might bind keys in unexpected ways (e.g. LEFT/RIGHT in singleton list);
wenzelm
parents:
53397
diff
changeset
|
292 |
case KeyEvent.VK_DOWN | KeyEvent.VK_KP_DOWN => move_items(1); e.consume |
53226
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
293 |
case KeyEvent.VK_PAGE_UP => move_pages(-1); e.consume |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
294 |
case KeyEvent.VK_PAGE_DOWN => move_pages(1); e.consume |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
295 |
case _ => |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
296 |
if (e.isActionKey || e.isAltDown || e.isMetaDown || e.isControlDown) |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
297 |
hide_popup() |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
298 |
} |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
299 |
} |
53232 | 300 |
propagate(e) |
53226
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
301 |
}, |
53232 | 302 |
key_typed = propagate _ |
53226
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
303 |
) |
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
|
304 |
|
53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
305 |
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
|
306 |
|
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
|
307 |
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
|
308 |
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
|
309 |
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
|
310 |
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
|
311 |
} |
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
|
312 |
}) |
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
|
313 |
|
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
|
314 |
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
|
315 |
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
|
316 |
}) |
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
|
317 |
|
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
|
318 |
|
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
|
319 |
/* 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
|
320 |
|
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
|
321 |
override def getFocusTraversalKeysEnabled = false |
53297 | 322 |
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
|
323 |
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
|
324 |
|
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
|
325 |
|
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
|
326 |
/* 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
|
327 |
|
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
|
328 |
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
|
329 |
{ |
53247
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53246
diff
changeset
|
330 |
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
|
331 |
val size = |
53230 | 332 |
{ |
333 |
val geometry = JEdit_Lib.window_geometry(completion, completion) |
|
334 |
val bounds = Rendering.popup_bounds |
|
53247
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53246
diff
changeset
|
335 |
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
|
336 |
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
|
337 |
new Dimension(w, h) |
53230 | 338 |
} |
53247
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53246
diff
changeset
|
339 |
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
|
340 |
} |
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
|
341 |
|
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
|
342 |
private def show_popup() |
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
|
343 |
{ |
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
|
344 |
popup.show |
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
|
345 |
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
|
346 |
} |
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
|
347 |
|
53232 | 348 |
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
|
349 |
{ |
53234
ea4abbbe1702
more careful refocus operation: do not reset focus if it was already lost (relevant when activating a different GUI component, for example);
wenzelm
parents:
53233
diff
changeset
|
350 |
val had_focus = list_view.peer.isFocusOwner |
53229
6ce8328d7912
explicit "hidden" operation with focus management;
wenzelm
parents:
53228
diff
changeset
|
351 |
popup.hide |
53234
ea4abbbe1702
more careful refocus operation: do not reset focus if it was already lost (relevant when activating a different GUI component, for example);
wenzelm
parents:
53233
diff
changeset
|
352 |
if (had_focus) refocus() |
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
|
353 |
} |
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
|
354 |
} |
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
|
355 |