equal
deleted
inserted
replaced
10 import isabelle._ |
10 import isabelle._ |
11 |
11 |
12 import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent} |
12 import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent} |
13 import javax.swing.{JComponent, JTextField} |
13 import javax.swing.{JComponent, JTextField} |
14 |
14 |
15 import scala.swing.{Button, Component, TextField, Label, ListView, TabbedPane, BorderPanel} |
15 import scala.swing.{Component, TextField, Label, ListView, TabbedPane, BorderPanel} |
16 import scala.swing.event.{SelectionChanged, ButtonClicked, Key, KeyPressed} |
16 import scala.swing.event.{SelectionChanged, Key, KeyPressed} |
17 |
17 |
18 import org.gjt.sp.jedit.View |
18 import org.gjt.sp.jedit.View |
19 |
19 |
20 |
20 |
21 object Query_Dockable { |
21 object Query_Dockable { |
108 private val allow_dups = new GUI.Bool("Duplicates") { |
108 private val allow_dups = new GUI.Bool("Duplicates") { |
109 tooltip = "Show all versions of matching theorems" |
109 tooltip = "Show all versions of matching theorems" |
110 override def clicked(): Unit = apply_query() |
110 override def clicked(): Unit = apply_query() |
111 } |
111 } |
112 |
112 |
113 private val apply_button = new Button("<html><b>Apply</b></html>") { |
113 private val apply_button = new GUI.Button("<html><b>Apply</b></html>") { |
114 tooltip = "Find theorems meeting specified criteria" |
114 tooltip = "Find theorems meeting specified criteria" |
115 reactions += { case ButtonClicked(_) => apply_query() } |
115 override def clicked(): Unit = apply_query() |
116 } |
116 } |
117 |
117 |
118 private val control_panel = |
118 private val control_panel = |
119 Wrap_Panel( |
119 Wrap_Panel( |
120 List(query_label, Component.wrap(query), limit, allow_dups, |
120 List(query_label, Component.wrap(query), limit, allow_dups, |
157 } |
157 } |
158 |
158 |
159 |
159 |
160 /* GUI page */ |
160 /* GUI page */ |
161 |
161 |
162 private val apply_button = new Button("<html><b>Apply</b></html>") { |
162 private val apply_button = new GUI.Button("<html><b>Apply</b></html>") { |
163 tooltip = "Find constants by name / type patterns" |
163 tooltip = "Find constants by name / type patterns" |
164 reactions += { case ButtonClicked(_) => apply_query() } |
164 override def clicked(): Unit = apply_query() |
165 } |
165 } |
166 |
166 |
167 private val control_panel = |
167 private val control_panel = |
168 Wrap_Panel( |
168 Wrap_Panel( |
169 List( |
169 List( |
231 update_items() |
231 update_items() |
232 |
232 |
233 |
233 |
234 /* GUI page */ |
234 /* GUI page */ |
235 |
235 |
236 private val apply_button = new Button("<html><b>Apply</b></html>") { |
236 private val apply_button = new GUI.Button("<html><b>Apply</b></html>") { |
237 tooltip = "Apply to current context" |
237 tooltip = "Apply to current context" |
|
238 override def clicked(): Unit = apply_query() |
|
239 |
238 listenTo(keys) |
240 listenTo(keys) |
239 reactions += { |
241 reactions += { |
240 case ButtonClicked(_) => apply_query() |
|
241 case evt @ KeyPressed(_, Key.Enter, 0, _) => |
242 case evt @ KeyPressed(_, Key.Enter, 0, _) => |
242 evt.peer.consume() |
243 evt.peer.consume() |
243 apply_query() |
244 apply_query() |
244 } |
245 } |
245 } |
246 } |