equal
deleted
inserted
replaced
249 |
249 |
250 /* GUI page */ |
250 /* GUI page */ |
251 |
251 |
252 private val apply_button = new Button("<html><b>Apply</b></html>") { |
252 private val apply_button = new Button("<html><b>Apply</b></html>") { |
253 tooltip = "Apply to current context" |
253 tooltip = "Apply to current context" |
254 reactions += { case ButtonClicked(_) => apply_query() } |
254 listenTo(keys) |
|
255 reactions += { |
|
256 case ButtonClicked(_) => apply_query() |
|
257 case evt @ KeyPressed(_, Key.Enter, 0, _) => |
|
258 evt.peer.consume |
|
259 apply_query() |
|
260 } |
255 } |
261 } |
256 |
262 |
257 private val control_panel = new Wrap_Panel(Wrap_Panel.Alignment.Right)() |
263 private val control_panel = new Wrap_Panel(Wrap_Panel.Alignment.Right)() |
258 |
264 |
259 def select |
265 def select |