8 |
8 |
9 |
9 |
10 import isabelle._ |
10 import isabelle._ |
11 |
11 |
12 import java.awt.{Point, BorderLayout, Dimension} |
12 import java.awt.{Point, BorderLayout, Dimension} |
13 import java.awt.event.{KeyEvent, KeyAdapter, MouseEvent, MouseAdapter, FocusAdapter, FocusEvent} |
13 import java.awt.event.{KeyEvent, MouseEvent, MouseAdapter, FocusAdapter, FocusEvent} |
14 import javax.swing.{JPanel, JComponent, PopupFactory} |
14 import javax.swing.{JPanel, JComponent, PopupFactory} |
15 |
15 |
16 import scala.swing.{ListView, ScrollPane} |
16 import scala.swing.{ListView, ScrollPane} |
17 import scala.swing.event.MouseClicked |
17 import scala.swing.event.MouseClicked |
18 |
18 |
19 import org.gjt.sp.jedit.View |
19 import org.gjt.sp.jedit.View |
|
20 import org.gjt.sp.jedit.gui.KeyEventWorkaround |
20 |
21 |
21 |
22 |
22 object Completion_Popup |
23 object Completion_Popup |
23 { |
24 { |
24 sealed case class Item(name: String, text: String) |
25 sealed case class Item(name: String, text: String) |
90 } |
91 } |
91 |
92 |
92 |
93 |
93 /* event handling */ |
94 /* event handling */ |
94 |
95 |
95 private val key_handler = new KeyAdapter { |
96 private val key_listener = |
96 override def keyPressed(e: KeyEvent) |
97 JEdit_Lib.key_listener( |
97 { |
98 workaround = false, |
98 if (!e.isConsumed) { |
99 key_pressed = (e: KeyEvent) => |
99 e.getKeyCode match { |
100 { |
100 case KeyEvent.VK_TAB => |
101 if (!e.isConsumed) { |
101 if (complete_selected()) e.consume |
102 e.getKeyCode match { |
102 hide_popup() |
103 case KeyEvent.VK_TAB => |
103 case KeyEvent.VK_ESCAPE => |
104 if (complete_selected()) e.consume |
104 hide_popup() |
105 hide_popup() |
105 e.consume |
106 case KeyEvent.VK_ESCAPE => |
106 case KeyEvent.VK_UP => move_items(-1); e.consume |
107 hide_popup() |
107 case KeyEvent.VK_DOWN => move_items(1); e.consume |
108 e.consume |
108 case KeyEvent.VK_PAGE_UP => move_pages(-1); e.consume |
109 case KeyEvent.VK_UP => move_items(-1); e.consume |
109 case KeyEvent.VK_PAGE_DOWN => move_pages(1); e.consume |
110 case KeyEvent.VK_DOWN => move_items(1); e.consume |
110 case _ => |
111 case KeyEvent.VK_PAGE_UP => move_pages(-1); e.consume |
111 if (e.isActionKey || e.isAltDown || e.isMetaDown || e.isControlDown) |
112 case KeyEvent.VK_PAGE_DOWN => move_pages(1); e.consume |
112 hide_popup() |
113 case _ => |
|
114 if (e.isActionKey || e.isAltDown || e.isMetaDown || e.isControlDown) |
|
115 hide_popup() |
|
116 } |
|
117 } |
|
118 if (!e.isConsumed) pass_to_view(e) |
|
119 }, |
|
120 key_typed = (e: KeyEvent) => |
|
121 { |
|
122 if (!e.isConsumed) pass_to_view(e) |
113 } |
123 } |
114 } |
124 ) |
115 if (!e.isConsumed) pass_to_view(e) |
|
116 } |
|
117 |
|
118 override def keyTyped(e: KeyEvent) |
|
119 { |
|
120 if (!e.isConsumed) pass_to_view(e) |
|
121 } |
|
122 } |
|
123 |
125 |
124 private def pass_to_view(e: KeyEvent) |
126 private def pass_to_view(e: KeyEvent) |
125 { |
127 { |
126 opt_view match { |
128 opt_view match { |
127 case Some(view) if view.getKeyEventInterceptor == key_handler => |
129 case Some(view) if view.getKeyEventInterceptor == key_listener => |
128 try { |
130 try { |
129 view.setKeyEventInterceptor(null) |
131 view.setKeyEventInterceptor(null) |
130 view.getInputHandler().processKeyEvent(e, View.ACTION_BAR, false) |
132 view.getInputHandler().processKeyEvent(e, View.ACTION_BAR, false) |
131 } |
133 } |
132 finally { view.setKeyEventInterceptor(key_handler) } |
134 finally { view.setKeyEventInterceptor(key_listener) } |
133 case _ => |
135 case _ => |
134 } |
136 } |
135 } |
137 } |
136 |
138 |
137 list_view.peer.addKeyListener(key_handler) |
139 list_view.peer.addKeyListener(key_listener) |
138 |
140 |
139 list_view.peer.addMouseListener(new MouseAdapter { |
141 list_view.peer.addMouseListener(new MouseAdapter { |
140 override def mouseClicked(e: MouseEvent) { |
142 override def mouseClicked(e: MouseEvent) { |
141 if (complete_selected()) e.consume |
143 if (complete_selected()) e.consume |
142 hide_popup() |
144 hide_popup() |
174 PopupFactory.getSharedInstance.getPopup(parent, completion, x, y) |
176 PopupFactory.getSharedInstance.getPopup(parent, completion, x, y) |
175 } |
177 } |
176 |
178 |
177 def show_popup() |
179 def show_popup() |
178 { |
180 { |
179 opt_view.foreach(view => view.setKeyEventInterceptor(key_handler)) |
181 opt_view.foreach(view => view.setKeyEventInterceptor(key_listener)) |
180 popup.show |
182 popup.show |
181 list_view.requestFocus |
183 list_view.requestFocus |
182 } |
184 } |
183 |
185 |
184 def hide_popup() |
186 def hide_popup() |
185 { |
187 { |
186 opt_view match { |
188 opt_view match { |
187 case Some(view) if view.getKeyEventInterceptor == key_handler => |
189 case Some(view) if view.getKeyEventInterceptor == key_listener => |
188 view.setKeyEventInterceptor(null) |
190 view.setKeyEventInterceptor(null) |
189 case _ => |
191 case _ => |
190 } |
192 } |
191 popup.hide |
193 popup.hide |
192 parent.requestFocus |
194 parent.requestFocus |