author | wenzelm |
Tue, 27 Aug 2013 12:35:32 +0200 | |
changeset 53226 | 9cf8e2263ca7 |
parent 53023 | f127e949389f |
child 53228 | f6c6688961db |
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 |
|
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
4 |
Completion popup based on javax.swing.PopupFactory. |
f127e949389f
Completion popup 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 |
|
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
12 |
import java.awt.{Point, BorderLayout, Dimension} |
53226
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
13 |
import java.awt.event.{KeyEvent, MouseEvent, MouseAdapter, FocusAdapter, FocusEvent} |
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
|
14 |
import javax.swing.{JPanel, JComponent, PopupFactory} |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
15 |
|
f127e949389f
Completion popup 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 |
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
|
17 |
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
|
18 |
|
f127e949389f
Completion popup 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 org.gjt.sp.jedit.View |
53226
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
20 |
import org.gjt.sp.jedit.gui.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
|
21 |
|
f127e949389f
Completion popup 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 |
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
|
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 |
sealed case class Item(name: String, text: String) |
f127e949389f
Completion popup 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 |
{ override def toString: String = text } |
f127e949389f
Completion popup 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 |
|
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
28 |
def apply( |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
29 |
opt_view: Option[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
|
30 |
parent: 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
|
31 |
screen_point: Point, |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
32 |
items: List[Item], |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
33 |
complete: Item => Unit): 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
|
34 |
{ |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
35 |
Swing_Thread.require() |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
36 |
|
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
37 |
require(!items.isEmpty) |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
38 |
|
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
39 |
val completion = new Completion_Popup(opt_view, parent, screen_point, items, complete) |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
40 |
completion.show_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
|
41 |
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
|
42 |
} |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
43 |
} |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
44 |
|
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
45 |
|
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
46 |
class Completion_Popup private( |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
47 |
opt_view: Option[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
|
48 |
parent: 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
|
49 |
screen_point: Point, |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
50 |
items: List[Completion_Popup.Item], |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
51 |
complete: Completion_Popup.Item => Unit) extends JPanel(new BorderLayout) |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
52 |
{ |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
53 |
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
|
54 |
|
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
55 |
Swing_Thread.require() |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
56 |
|
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
57 |
|
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
58 |
/* 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
|
59 |
|
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
60 |
private val list_view = new ListView(items) |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
61 |
{ |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
62 |
font = parent.getFont |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
63 |
} |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
64 |
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
|
65 |
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
|
66 |
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
|
67 |
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
|
68 |
|
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
69 |
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
|
70 |
{ |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
71 |
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
|
72 |
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
|
73 |
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
|
74 |
} |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
75 |
} |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
76 |
|
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
77 |
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
|
78 |
{ |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
79 |
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
|
80 |
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
|
81 |
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
|
82 |
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
|
83 |
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
|
84 |
} |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
85 |
} |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
86 |
|
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
87 |
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
|
88 |
{ |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
89 |
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
|
90 |
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
|
91 |
} |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
92 |
|
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
93 |
|
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
94 |
/* 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
|
95 |
|
53226
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
96 |
private val key_listener = |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
97 |
JEdit_Lib.key_listener( |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
98 |
workaround = false, |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
99 |
key_pressed = (e: KeyEvent) => |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
100 |
{ |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
101 |
if (!e.isConsumed) { |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
102 |
e.getKeyCode match { |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
103 |
case KeyEvent.VK_TAB => |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
104 |
if (complete_selected()) e.consume |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
105 |
hide_popup() |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
106 |
case KeyEvent.VK_ESCAPE => |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
107 |
hide_popup() |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
108 |
e.consume |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
109 |
case KeyEvent.VK_UP => move_items(-1); e.consume |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
110 |
case KeyEvent.VK_DOWN => move_items(1); e.consume |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
111 |
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
|
112 |
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
|
113 |
case _ => |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
114 |
if (e.isActionKey || e.isAltDown || e.isMetaDown || e.isControlDown) |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
115 |
hide_popup() |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
116 |
} |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
117 |
} |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
118 |
if (!e.isConsumed) pass_to_view(e) |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
119 |
}, |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
120 |
key_typed = (e: KeyEvent) => |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
121 |
{ |
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
122 |
if (!e.isConsumed) pass_to_view(e) |
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
|
123 |
} |
53226
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
124 |
) |
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
|
125 |
|
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
126 |
private def pass_to_view(e: KeyEvent) |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
127 |
{ |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
128 |
opt_view match { |
53226
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
129 |
case Some(view) if view.getKeyEventInterceptor == 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
|
130 |
try { |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
131 |
view.setKeyEventInterceptor(null) |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
132 |
view.getInputHandler().processKeyEvent(e, View.ACTION_BAR, 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
|
133 |
} |
53226
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
134 |
finally { view.setKeyEventInterceptor(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
|
135 |
case _ => |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
136 |
} |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
137 |
} |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
138 |
|
53226
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
139 |
list_view.peer.addKeyListener(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
|
140 |
|
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
141 |
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
|
142 |
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
|
143 |
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
|
144 |
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
|
145 |
} |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
146 |
}) |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
147 |
|
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
148 |
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
|
149 |
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
|
150 |
}) |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
151 |
|
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
152 |
|
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
153 |
/* 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
|
154 |
|
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
155 |
override def getFocusTraversalKeysEnabled = 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
|
156 |
|
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
157 |
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
|
158 |
|
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
159 |
|
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
160 |
/* 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
|
161 |
|
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
162 |
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
|
163 |
{ |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
164 |
val screen_bounds = JEdit_Lib.screen_bounds(screen_point) |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
165 |
|
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
166 |
val geometry = JEdit_Lib.window_geometry(completion, 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
|
167 |
|
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
168 |
val w = geometry.width min (screen_bounds.width / 2) |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
169 |
val h = geometry.height min (screen_bounds.height / 2) |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
170 |
|
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
171 |
completion.setSize(new Dimension(w, h)) |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
172 |
completion.setPreferredSize(new Dimension(w, h)) |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
173 |
|
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
174 |
val x = screen_point.x min (screen_bounds.x + screen_bounds.width - w) |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
175 |
val y = screen_point.y min (screen_bounds.y + screen_bounds.height - h) |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
176 |
PopupFactory.getSharedInstance.getPopup(parent, completion, x, y) |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
177 |
} |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
178 |
|
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
179 |
def show_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
|
180 |
{ |
53226
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
181 |
opt_view.foreach(view => view.setKeyEventInterceptor(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
|
182 |
popup.show |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
183 |
list_view.requestFocus |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
184 |
} |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
185 |
|
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
186 |
def 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
|
187 |
{ |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
188 |
opt_view match { |
53226
9cf8e2263ca7
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
wenzelm
parents:
53023
diff
changeset
|
189 |
case Some(view) if view.getKeyEventInterceptor == 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
|
190 |
view.setKeyEventInterceptor(null) |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
191 |
case _ => |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
192 |
} |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
193 |
popup.hide |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
194 |
parent.requestFocus |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
195 |
} |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
196 |
} |
f127e949389f
Completion popup based on javax.swing.PopupFactory, which has better cross-platform chances than JWindow (cf. org/gjt/jedit/gui/CompletionPopup.java);
wenzelm
parents:
diff
changeset
|
197 |