author | wenzelm |
Tue, 25 Feb 2014 20:57:57 +0100 | |
changeset 55749 | 75a48dc4383e |
parent 55748 | 2e1398b484aa |
child 55752 | 43d0e2a34c9d |
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} |
53784 | 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 | 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 | 21 |
import org.gjt.sp.jedit.View |
55712 | 22 |
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea} |
53784 | 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 |
{ |
53784 | 28 |
/** 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
|
29 |
|
53242 | 30 |
object Text_Area |
53233 | 31 |
{ |
53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
32 |
private val key = new Object |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
33 |
|
55712 | 34 |
def apply(text_area: TextArea): Option[Completion_Popup.Text_Area] = |
35 |
{ |
|
36 |
Swing_Thread.require() |
|
53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
37 |
text_area.getClientProperty(key) match { |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
38 |
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
|
39 |
case _ => None |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
40 |
} |
55712 | 41 |
} |
53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
42 |
|
55712 | 43 |
def active_range(text_area: TextArea): Option[Text.Range] = |
44 |
apply(text_area) match { |
|
45 |
case Some(text_area_completion) => text_area_completion.active_range |
|
46 |
case None => None |
|
55711 | 47 |
} |
48 |
||
53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
49 |
def exit(text_area: JEditTextArea) |
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 |
Swing_Thread.require() |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
52 |
apply(text_area) match { |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
53 |
case None => |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
54 |
case Some(text_area_completion) => |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
55 |
text_area_completion.deactivate() |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
56 |
text_area.putClientProperty(key, null) |
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 |
} |
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 |
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
|
61 |
{ |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
62 |
exit(text_area) |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
63 |
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
|
64 |
text_area.putClientProperty(key, text_area_completion) |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
65 |
text_area_completion.activate() |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
66 |
text_area_completion |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
67 |
} |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
68 |
|
55712 | 69 |
def dismissed(text_area: TextArea): Boolean = |
53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
70 |
{ |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
71 |
Swing_Thread.require() |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
72 |
apply(text_area) match { |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
73 |
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
|
74 |
case None => false |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
75 |
} |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
76 |
} |
53272 | 77 |
} |
78 |
||
53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
79 |
class Text_Area private(text_area: JEditTextArea) |
53272 | 80 |
{ |
55711 | 81 |
// owned by Swing thread |
53272 | 82 |
private var completion_popup: Option[Completion_Popup] = None |
83 |
||
55711 | 84 |
def active_range: Option[Text.Range] = |
85 |
completion_popup match { |
|
86 |
case Some(completion) => |
|
87 |
completion.active_range match { |
|
88 |
case Some((range, _)) if completion.isDisplayable => Some(range) |
|
89 |
case _ => None |
|
90 |
} |
|
91 |
case None => None |
|
92 |
} |
|
93 |
||
53272 | 94 |
|
55747
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
95 |
/* rendering */ |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
96 |
|
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
97 |
def rendering(rendering: Rendering, line_range: Text.Range): Option[Text.Info[Color]] = |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
98 |
{ |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
99 |
active_range match { |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
100 |
case Some(range) => range.try_restrict(line_range) |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
101 |
case None => |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
102 |
val buffer = text_area.getBuffer |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
103 |
val caret = text_area.getCaretPosition |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
104 |
|
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
105 |
if (line_range.contains(caret)) { |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
106 |
JEdit_Lib.stretch_point_range(buffer, caret).try_restrict(line_range) match { |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
107 |
case Some(range) if !range.is_singularity => |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
108 |
rendering.completion_names(range) match { |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
109 |
case Some(names) => Some(names.range) |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
110 |
case None => |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
111 |
syntax_completion(Some(rendering), false) match { |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
112 |
case Some(result) => Some(result.range) |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
113 |
case None => None |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
114 |
} |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
115 |
} |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
116 |
case _ => None |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
117 |
} |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
118 |
} |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
119 |
else None |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
120 |
} |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
121 |
}.map(range => Text.Info(range, rendering.completion_color)) |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
122 |
|
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
123 |
|
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
124 |
/* syntax completion */ |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
125 |
|
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
126 |
def syntax_completion( |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
127 |
opt_rendering: Option[Rendering], explicit: Boolean): Option[Completion.Result] = |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
128 |
{ |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
129 |
val buffer = text_area.getBuffer |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
130 |
val history = PIDE.completion_history.value |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
131 |
val decode = Isabelle_Encoding.is_active(buffer) |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
132 |
|
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
133 |
Isabelle.mode_syntax(JEdit_Lib.buffer_mode(buffer)) match { |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
134 |
case Some(syntax) => |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
135 |
val caret = text_area.getCaretPosition |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
136 |
val line = buffer.getLineOfOffset(caret) |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
137 |
val start = buffer.getLineStartOffset(line) |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
138 |
val text = buffer.getSegment(start, caret - start) |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
139 |
|
55748 | 140 |
val word_context = |
141 |
Completion.word_context( |
|
142 |
JEdit_Lib.try_get_text(buffer, JEdit_Lib.point_range(buffer, caret))) |
|
143 |
||
55747
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
144 |
val context = |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
145 |
(opt_rendering orElse PIDE.document_view(text_area).map(_.get_rendering()) match { |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
146 |
case Some(rendering) => |
55749 | 147 |
rendering.language_context(JEdit_Lib.stretch_point_range(buffer, caret)) |
55747
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
148 |
case None => None |
55749 | 149 |
}) getOrElse syntax.language_context |
55747
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
150 |
|
55748 | 151 |
syntax.completion.complete(history, decode, explicit, start, text, word_context, context) |
55747
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
152 |
|
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
153 |
case None => None |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
154 |
} |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
155 |
} |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
156 |
|
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
157 |
|
53292
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
158 |
/* completion action */ |
53273 | 159 |
|
53275 | 160 |
private def insert(item: Completion.Item) |
53242 | 161 |
{ |
162 |
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
|
163 |
|
53242 | 164 |
val buffer = text_area.getBuffer |
55692
19e8b00684f7
more explicit Completion.Item.range, independently of caret;
wenzelm
parents:
55690
diff
changeset
|
165 |
val range = item.range |
19e8b00684f7
more explicit Completion.Item.range, independently of caret;
wenzelm
parents:
55690
diff
changeset
|
166 |
if (buffer.isEditable && range.length > 0) { |
53242 | 167 |
JEdit_Lib.buffer_edit(buffer) { |
55692
19e8b00684f7
more explicit Completion.Item.range, independently of caret;
wenzelm
parents:
55690
diff
changeset
|
168 |
JEdit_Lib.try_get_text(buffer, range) match { |
53242 | 169 |
case Some(text) if text == item.original => |
55692
19e8b00684f7
more explicit Completion.Item.range, independently of caret;
wenzelm
parents:
55690
diff
changeset
|
170 |
buffer.remove(range.start, range.length) |
19e8b00684f7
more explicit Completion.Item.range, independently of caret;
wenzelm
parents:
55690
diff
changeset
|
171 |
buffer.insert(range.start, item.replacement) |
19e8b00684f7
more explicit Completion.Item.range, independently of caret;
wenzelm
parents:
55690
diff
changeset
|
172 |
text_area.moveCaretPosition(range.start + item.replacement.length + item.move) |
53242 | 173 |
case _ => |
174 |
} |
|
53233 | 175 |
} |
176 |
} |
|
177 |
} |
|
53242 | 178 |
|
53322 | 179 |
def action(immediate: Boolean = false, explicit: Boolean = false) |
53292
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
180 |
{ |
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
181 |
val view = text_area.getView |
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
182 |
val layered = view.getLayeredPane |
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
183 |
val buffer = text_area.getBuffer |
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
184 |
val painter = text_area.getPainter |
55693
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
185 |
val caret = text_area.getCaretPosition |
53273 | 186 |
|
55693
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
187 |
val history = PIDE.completion_history.value |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
188 |
val decode = Isabelle_Encoding.is_active(buffer) |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
189 |
|
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
190 |
def open_popup(result: Completion.Result) |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
191 |
{ |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
192 |
val font = |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
193 |
painter.getFont.deriveFont(Rendering.font_size("jedit_popup_font_scale")) |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
194 |
|
55711 | 195 |
val range = result.range |
196 |
def invalidate(): Unit = JEdit_Lib.invalidate_range(text_area, range) |
|
197 |
||
198 |
val loc1 = text_area.offsetToXY(range.start) |
|
55693
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
199 |
if (loc1 != null) { |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
200 |
val loc2 = |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
201 |
SwingUtilities.convertPoint(painter, |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
202 |
loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered) |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
203 |
|
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
204 |
val completion = |
55711 | 205 |
new Completion_Popup(Some((range, invalidate _)), layered, loc2, font, result.items) { |
55693
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
206 |
override def complete(item: Completion.Item) { |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
207 |
PIDE.completion_history.update(item) |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
208 |
insert(item) |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
209 |
} |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
210 |
override def propagate(evt: KeyEvent) { |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
211 |
JEdit_Lib.propagate_key(view, evt) |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
212 |
input(evt) |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
213 |
} |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
214 |
override def refocus() { text_area.requestFocus } |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
215 |
} |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
216 |
completion_popup = Some(completion) |
55711 | 217 |
invalidate() |
55693
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
218 |
completion.show_popup() |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
219 |
} |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
220 |
} |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
221 |
|
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
222 |
def semantic_completion(): Boolean = |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
223 |
explicit && { |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
224 |
PIDE.document_view(text_area) match { |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
225 |
case Some(doc_view) => |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
226 |
val rendering = doc_view.get_rendering() |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
227 |
rendering.completion_names(JEdit_Lib.stretch_point_range(buffer, caret)) match { |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
228 |
case None => false |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
229 |
case Some(names) => |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
230 |
JEdit_Lib.try_get_text(buffer, names.range) match { |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
231 |
case Some(original) => |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
232 |
names.complete(history, decode, original) match { |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
233 |
case Some(result) if !result.items.isEmpty => |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
234 |
open_popup(result) |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
235 |
true |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
236 |
case _ => false |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
237 |
} |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
238 |
case None => false |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
239 |
} |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
240 |
} |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
241 |
case _ => false |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
242 |
} |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
243 |
} |
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
244 |
|
55747
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
245 |
def syntactic_completion(): Boolean = |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
246 |
syntax_completion(None, explicit) match { |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
247 |
case Some(result) => |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
248 |
result.items match { |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
249 |
case List(item) if result.unique && item.immediate && immediate => |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
250 |
insert(item); true |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
251 |
case _ :: _ => open_popup(result); true |
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
252 |
case _ => false |
53292
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
253 |
} |
55693
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
254 |
case None => false |
53292
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
255 |
} |
55693
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
256 |
|
93ba0085e888
try explicit semantic completion before syntax completion;
wenzelm
parents:
55692
diff
changeset
|
257 |
if (buffer.isEditable) |
55747
bef19c929ba5
more completion rendering: active, semantic, syntactic;
wenzelm
parents:
55712
diff
changeset
|
258 |
semantic_completion() || syntactic_completion() |
53292
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
259 |
} |
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
260 |
|
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
261 |
|
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
262 |
/* input key events */ |
53273 | 263 |
|
53272 | 264 |
def input(evt: KeyEvent) |
53242 | 265 |
{ |
266 |
Swing_Thread.require() |
|
53233 | 267 |
|
53273 | 268 |
if (PIDE.options.bool("jedit_completion")) { |
269 |
if (!evt.isConsumed) { |
|
270 |
dismissed() |
|
53397
b179cdfa9d82
no completion on backspace -- too intrusive, e.g. when deleting keywords;
wenzelm
parents:
53337
diff
changeset
|
271 |
if (evt.getKeyChar != '\b') { |
53784 | 272 |
val special = JEdit_Lib.special_key(evt) |
53397
b179cdfa9d82
no completion on backspace -- too intrusive, e.g. when deleting keywords;
wenzelm
parents:
53337
diff
changeset
|
273 |
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
|
274 |
input_delay.revoke() |
b179cdfa9d82
no completion on backspace -- too intrusive, e.g. when deleting keywords;
wenzelm
parents:
53337
diff
changeset
|
275 |
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
|
276 |
} |
b179cdfa9d82
no completion on backspace -- too intrusive, e.g. when deleting keywords;
wenzelm
parents:
53337
diff
changeset
|
277 |
else input_delay.invoke() |
53292
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
278 |
} |
53242 | 279 |
} |
53228
f6c6688961db
some key event handling in the manner of SideKickBindings, SideKickCompletionPopup;
wenzelm
parents:
53226
diff
changeset
|
280 |
} |
f6c6688961db
some key event handling in the manner of SideKickBindings, SideKickCompletionPopup;
wenzelm
parents:
53226
diff
changeset
|
281 |
} |
53273 | 282 |
|
283 |
private val input_delay = |
|
53292
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
284 |
Swing_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay")) { |
53322 | 285 |
action() |
53292
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
286 |
} |
53273 | 287 |
|
288 |
||
53292
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
289 |
/* dismiss popup */ |
53273 | 290 |
|
53292
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
291 |
def dismissed(): Boolean = |
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
292 |
{ |
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
293 |
Swing_Thread.require() |
53273 | 294 |
|
53292
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
295 |
completion_popup match { |
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
296 |
case Some(completion) => |
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
297 |
completion.hide_popup() |
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
298 |
completion_popup = None |
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
299 |
true |
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
300 |
case None => |
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
301 |
false |
53273 | 302 |
} |
53292
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53275
diff
changeset
|
303 |
} |
53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
304 |
|
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
305 |
|
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
306 |
/* activation */ |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
307 |
|
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
308 |
private val outer_key_listener = |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
309 |
JEdit_Lib.key_listener(key_typed = input _) |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
310 |
|
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
311 |
private def activate() |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
312 |
{ |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
313 |
text_area.addKeyListener(outer_key_listener) |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
314 |
} |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
315 |
|
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
316 |
private def deactivate() |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
317 |
{ |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
318 |
dismissed() |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
319 |
text_area.removeKeyListener(outer_key_listener) |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
320 |
} |
53228
f6c6688961db
some key event handling in the manner of SideKickBindings, SideKickCompletionPopup;
wenzelm
parents:
53226
diff
changeset
|
321 |
} |
53784 | 322 |
|
323 |
||
324 |
||
325 |
/** history text field **/ |
|
326 |
||
327 |
class History_Text_Field( |
|
328 |
name: String = null, |
|
329 |
instant_popups: Boolean = false, |
|
330 |
enter_adds_to_history: Boolean = true, |
|
331 |
syntax: Outer_Syntax = Outer_Syntax.init) extends |
|
332 |
HistoryTextField(name, instant_popups, enter_adds_to_history) |
|
333 |
{ |
|
334 |
text_field => |
|
335 |
||
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
|
336 |
// 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
|
337 |
if (GUI.is_macos_laf) text_field.setCaret(new DefaultCaret) |
53784 | 338 |
|
55711 | 339 |
// owned by Swing thread |
53784 | 340 |
private var completion_popup: Option[Completion_Popup] = None |
341 |
||
342 |
||
343 |
/* dismiss */ |
|
344 |
||
345 |
private def dismissed(): Boolean = |
|
346 |
{ |
|
347 |
completion_popup match { |
|
348 |
case Some(completion) => |
|
349 |
completion.hide_popup() |
|
350 |
completion_popup = None |
|
351 |
true |
|
352 |
case None => |
|
353 |
false |
|
354 |
} |
|
355 |
} |
|
356 |
||
357 |
||
358 |
/* insert */ |
|
359 |
||
360 |
private def insert(item: Completion.Item) |
|
361 |
{ |
|
362 |
Swing_Thread.require() |
|
363 |
||
55692
19e8b00684f7
more explicit Completion.Item.range, independently of caret;
wenzelm
parents:
55690
diff
changeset
|
364 |
val range = item.range |
19e8b00684f7
more explicit Completion.Item.range, independently of caret;
wenzelm
parents:
55690
diff
changeset
|
365 |
if (text_field.isEditable && range.length > 0) { |
53784 | 366 |
val content = text_field.getText |
55692
19e8b00684f7
more explicit Completion.Item.range, independently of caret;
wenzelm
parents:
55690
diff
changeset
|
367 |
JEdit_Lib.try_get_text(content, range) match { |
53784 | 368 |
case Some(text) if text == item.original => |
369 |
text_field.setText( |
|
55692
19e8b00684f7
more explicit Completion.Item.range, independently of caret;
wenzelm
parents:
55690
diff
changeset
|
370 |
content.substring(0, range.start) + |
53784 | 371 |
item.replacement + |
55692
19e8b00684f7
more explicit Completion.Item.range, independently of caret;
wenzelm
parents:
55690
diff
changeset
|
372 |
content.substring(range.stop)) |
19e8b00684f7
more explicit Completion.Item.range, independently of caret;
wenzelm
parents:
55690
diff
changeset
|
373 |
text_field.getCaret.setDot(range.start + item.replacement.length + item.move) |
53784 | 374 |
case _ => |
375 |
} |
|
376 |
} |
|
377 |
} |
|
378 |
||
379 |
||
380 |
/* completion action */ |
|
381 |
||
382 |
def action() |
|
383 |
{ |
|
384 |
GUI.layered_pane(text_field) match { |
|
385 |
case Some(layered) if text_field.isEditable => |
|
386 |
val history = PIDE.completion_history.value |
|
387 |
||
388 |
val caret = text_field.getCaret.getDot |
|
389 |
val text = text_field.getText.substring(0, caret) |
|
390 |
||
55748 | 391 |
val word_context = |
392 |
Completion.word_context(JEdit_Lib.try_get_text(text_field.getText, |
|
393 |
Text.Range(caret, caret + 1))) // FIXME proper point range!? |
|
394 |
||
55749 | 395 |
val context = syntax.language_context |
55748 | 396 |
|
397 |
syntax.completion.complete(history, true, false, 0, text, word_context, context) match { |
|
53784 | 398 |
case Some(result) => |
399 |
val fm = text_field.getFontMetrics(text_field.getFont) |
|
400 |
val loc = |
|
401 |
SwingUtilities.convertPoint(text_field, fm.stringWidth(text), fm.getHeight, layered) |
|
402 |
||
55711 | 403 |
val completion = |
404 |
new Completion_Popup(None, layered, loc, text_field.getFont, result.items) |
|
53784 | 405 |
{ |
406 |
override def complete(item: Completion.Item) { |
|
407 |
PIDE.completion_history.update(item) |
|
408 |
insert(item) |
|
409 |
} |
|
410 |
override def propagate(evt: KeyEvent) { |
|
411 |
if (!evt.isConsumed) text_field.processKeyEvent(evt) |
|
412 |
} |
|
413 |
override def refocus() { text_field.requestFocus } |
|
414 |
} |
|
415 |
completion_popup = Some(completion) |
|
416 |
completion.show_popup() |
|
417 |
||
418 |
case None => |
|
419 |
} |
|
420 |
case _ => |
|
421 |
} |
|
422 |
} |
|
423 |
||
424 |
||
425 |
/* process key event */ |
|
426 |
||
427 |
private def process(evt: KeyEvent) |
|
428 |
{ |
|
429 |
if (PIDE.options.bool("jedit_completion")) { |
|
430 |
dismissed() |
|
431 |
if (evt.getKeyChar != '\b') { |
|
432 |
val special = JEdit_Lib.special_key(evt) |
|
433 |
if (PIDE.options.seconds("jedit_completion_delay").is_zero && !special) { |
|
434 |
process_delay.revoke() |
|
435 |
action() |
|
436 |
} |
|
437 |
else process_delay.invoke() |
|
438 |
} |
|
439 |
} |
|
440 |
} |
|
441 |
||
442 |
private val process_delay = |
|
443 |
Swing_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay")) { |
|
444 |
action() |
|
445 |
} |
|
446 |
||
447 |
override def processKeyEvent(evt0: KeyEvent) |
|
448 |
{ |
|
449 |
val evt = KeyEventWorkaround.processKeyEvent(evt0) |
|
450 |
if (evt != null) { |
|
451 |
evt.getID match { |
|
452 |
case KeyEvent.KEY_PRESSED => |
|
453 |
val key_code = evt.getKeyCode |
|
454 |
if (key_code == KeyEvent.VK_ESCAPE) { |
|
455 |
if (dismissed()) evt.consume |
|
456 |
} |
|
457 |
case KeyEvent.KEY_TYPED => |
|
458 |
super.processKeyEvent(evt) |
|
459 |
process(evt) |
|
460 |
evt.consume |
|
461 |
case _ => |
|
462 |
} |
|
463 |
if (!evt.isConsumed) super.processKeyEvent(evt) |
|
464 |
} |
|
465 |
} |
|
466 |
} |
|
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
|
467 |
} |
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
|
468 |
|
53233 | 469 |
|
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
|
470 |
class Completion_Popup private( |
55711 | 471 |
val active_range: Option[(Text.Range, () => Unit)], |
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
|
472 |
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
|
473 |
location: Point, |
53272 | 474 |
font: Font, |
53275 | 475 |
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
|
476 |
{ |
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
|
477 |
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
|
478 |
|
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
|
479 |
Swing_Thread.require() |
53405 | 480 |
|
53232 | 481 |
require(!items.isEmpty) |
53405 | 482 |
val multi = items.length > 1 |
53232 | 483 |
|
484 |
||
485 |
/* actions */ |
|
486 |
||
53275 | 487 |
def complete(item: Completion.Item) { } |
53232 | 488 |
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
|
489 |
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
|
490 |
|
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
|
491 |
|
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
|
492 |
/* 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
|
493 |
|
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
|
494 |
private val list_view = new ListView(items) |
53272 | 495 |
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
|
496 |
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
|
497 |
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
|
498 |
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
|
499 |
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
|
500 |
|
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
|
501 |
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
|
502 |
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
|
503 |
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
|
504 |
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
|
505 |
|
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
|
506 |
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
|
507 |
{ |
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
|
508 |
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
|
509 |
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
|
510 |
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
|
511 |
} |
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
|
512 |
} |
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
|
513 |
|
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
|
514 |
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
|
515 |
{ |
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
|
516 |
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
|
517 |
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
|
518 |
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
|
519 |
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
|
520 |
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
|
521 |
} |
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
|
522 |
} |
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
|
523 |
|
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
|
524 |
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
|
525 |
{ |
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
|
526 |
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
|
527 |
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
|
528 |
} |
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
|
529 |
|
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
|
530 |
|
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
|
531 |
/* 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
|
532 |
|
53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
533 |
private val inner_key_listener = |
53226
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
534 |
JEdit_Lib.key_listener( |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
535 |
key_pressed = (e: KeyEvent) => |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
536 |
{ |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
537 |
if (!e.isConsumed) { |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
538 |
e.getKeyCode match { |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
539 |
case KeyEvent.VK_TAB => |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
540 |
if (complete_selected()) e.consume |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
541 |
hide_popup() |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
542 |
case KeyEvent.VK_ESCAPE => |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
543 |
hide_popup() |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
544 |
e.consume |
53405 | 545 |
case KeyEvent.VK_UP | KeyEvent.VK_KP_UP if multi => |
53407 | 546 |
move_items(-1) |
547 |
e.consume |
|
53405 | 548 |
case KeyEvent.VK_DOWN | KeyEvent.VK_KP_DOWN if multi => |
53407 | 549 |
move_items(1) |
550 |
e.consume |
|
53405 | 551 |
case KeyEvent.VK_PAGE_UP if multi => |
53407 | 552 |
move_pages(-1) |
553 |
e.consume |
|
53405 | 554 |
case KeyEvent.VK_PAGE_DOWN if multi => |
53407 | 555 |
move_pages(1) |
556 |
e.consume |
|
53226
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
557 |
case _ => |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
558 |
if (e.isActionKey || e.isAltDown || e.isMetaDown || e.isControlDown) |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
559 |
hide_popup() |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
560 |
} |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
561 |
} |
53232 | 562 |
propagate(e) |
53226
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
563 |
}, |
53232 | 564 |
key_typed = propagate _ |
53226
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
565 |
) |
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
|
566 |
|
53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53273
diff
changeset
|
567 |
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
|
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 |
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
|
570 |
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
|
571 |
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
|
572 |
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
|
573 |
} |
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
|
574 |
}) |
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
|
575 |
|
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
|
576 |
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
|
577 |
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
|
578 |
}) |
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 |
|
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
|
580 |
|
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
|
581 |
/* 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
|
582 |
|
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
|
583 |
override def getFocusTraversalKeysEnabled = false |
53297 | 584 |
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
|
585 |
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
|
586 |
|
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
|
587 |
|
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
|
588 |
/* 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
|
589 |
|
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
|
590 |
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
|
591 |
{ |
53247
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53246
diff
changeset
|
592 |
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
|
593 |
val size = |
53230 | 594 |
{ |
595 |
val geometry = JEdit_Lib.window_geometry(completion, completion) |
|
596 |
val bounds = Rendering.popup_bounds |
|
53247
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53246
diff
changeset
|
597 |
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
|
598 |
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
|
599 |
new Dimension(w, h) |
53230 | 600 |
} |
53247
bd595338ca18
uniform use of isabelle.jEdit.Popup, based on generic screen location operations;
wenzelm
parents:
53246
diff
changeset
|
601 |
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
|
602 |
} |
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
|
603 |
|
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
|
604 |
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
|
605 |
{ |
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
|
606 |
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
|
607 |
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
|
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 |
|
54377
750561986828
added jedit_completion_dismiss_delay for hide_popup, which helps to avoid loosing key events on old popup (no change of default behavior);
wenzelm
parents:
54376
diff
changeset
|
610 |
private val hide_popup_delay = |
750561986828
added jedit_completion_dismiss_delay for hide_popup, which helps to avoid loosing key events on old popup (no change of default behavior);
wenzelm
parents:
54376
diff
changeset
|
611 |
Swing_Thread.delay_last(PIDE.options.seconds("jedit_completion_dismiss_delay")) { |
55711 | 612 |
active_range match { case Some((_, invalidate)) => invalidate() case _ => } |
54377
750561986828
added jedit_completion_dismiss_delay for hide_popup, which helps to avoid loosing key events on old popup (no change of default behavior);
wenzelm
parents:
54376
diff
changeset
|
613 |
popup.hide |
750561986828
added jedit_completion_dismiss_delay for hide_popup, which helps to avoid loosing key events on old popup (no change of default behavior);
wenzelm
parents:
54376
diff
changeset
|
614 |
} |
750561986828
added jedit_completion_dismiss_delay for hide_popup, which helps to avoid loosing key events on old popup (no change of default behavior);
wenzelm
parents:
54376
diff
changeset
|
615 |
|
53232 | 616 |
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
|
617 |
{ |
54376
3eb84b6b0353
transfer focus before closing old component -- avoid intermediate focus switch to root component, which is actually visible e.g. on Windows;
wenzelm
parents:
53987
diff
changeset
|
618 |
if (list_view.peer.isFocusOwner) refocus() |
54377
750561986828
added jedit_completion_dismiss_delay for hide_popup, which helps to avoid loosing key events on old popup (no change of default behavior);
wenzelm
parents:
54376
diff
changeset
|
619 |
|
55711 | 620 |
if (PIDE.options.seconds("jedit_completion_dismiss_delay").is_zero) { |
621 |
active_range match { case Some((_, invalidate)) => invalidate() case _ => } |
|
54377
750561986828
added jedit_completion_dismiss_delay for hide_popup, which helps to avoid loosing key events on old popup (no change of default behavior);
wenzelm
parents:
54376
diff
changeset
|
622 |
popup.hide |
55711 | 623 |
} |
54377
750561986828
added jedit_completion_dismiss_delay for hide_popup, which helps to avoid loosing key events on old popup (no change of default behavior);
wenzelm
parents:
54376
diff
changeset
|
624 |
else hide_popup_delay.invoke() |
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
|
625 |
} |
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 |