--- a/src/Tools/jEdit/src/find_dockable.scala Sat Apr 26 18:06:21 2014 +0200
+++ b/src/Tools/jEdit/src/find_dockable.scala Sat Apr 26 21:16:50 2014 +0200
@@ -9,26 +9,58 @@
import isabelle._
-import scala.swing.{Button, Component, TextField, CheckBox, Label, ComboBox}
-import scala.swing.event.{ButtonClicked, Key, KeyPressed}
+import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent}
+import javax.swing.{JComponent, JTextField}
-import java.awt.BorderLayout
-import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent}
+import scala.swing.{Button, Component, TextField, CheckBox, Label,
+ ComboBox, TabbedPane, BorderPanel}
+import scala.swing.event.{ButtonClicked, Key, KeyPressed}
import org.gjt.sp.jedit.View
+object Find_Dockable
+{
+ private abstract class Operation
+ {
+ def query_operation: Query_Operation[View]
+ def query: JComponent
+ def pretty_text_area: Pretty_Text_Area
+ def page: TabbedPane.Page
+ }
+}
+
class Find_Dockable(view: View, position: String) extends Dockable(view, position)
{
- val pretty_text_area = new Pretty_Text_Area(view)
- set_content(pretty_text_area)
+ /* common GUI components */
+
+ private var zoom_factor = 100
+
+ private val zoom =
+ new GUI.Zoom_Box(factor => if (zoom_factor != factor) { zoom_factor = factor; handle_resize() })
+ {
+ tooltip = "Zoom factor for output font size"
+ }
- /* query operation */
+ private def make_query(property: String, tooltip: String, apply_query: () => Unit): JTextField =
+ new Completion_Popup.History_Text_Field(property)
+ {
+ override def processKeyEvent(evt: KeyEvent)
+ {
+ if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER) apply_query()
+ super.processKeyEvent(evt)
+ }
+ { val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) }
+ setColumns(40)
+ setToolTipText(tooltip)
+ setFont(GUI.imitate_font(Font_Info.main_family(), getFont, 1.2))
+ }
- private val process_indicator = new Process_Indicator
- private def consume_status(status: Query_Operation.Status.Value)
+ /* consume status */
+
+ def consume_status(process_indicator: Process_Indicator, status: Query_Operation.Status.Value)
{
status match {
case Query_Operation.Status.WAITING =>
@@ -40,23 +72,95 @@
}
}
- private val find_theorems =
- new Query_Operation(PIDE.editor, view, "find_theorems", consume_status _,
- (snapshot, results, body) =>
- pretty_text_area.update(snapshot, results, Pretty.separate(body)))
+
+ /* find theorems */
+
+ private val find_theorems = new Find_Dockable.Operation
+ {
+ val pretty_text_area = new Pretty_Text_Area(view)
+
+
+ /* query */
+
+ private val process_indicator = new Process_Indicator
+
+ val query_operation =
+ new Query_Operation(PIDE.editor, view, "find_theorems",
+ consume_status(process_indicator, _),
+ (snapshot, results, body) =>
+ pretty_text_area.update(snapshot, results, Pretty.separate(body)))
+
+ private def apply_query()
+ {
+ query_operation.apply_query(List(limit.text, allow_dups.selected.toString, query.getText))
+ }
+
+ private val query_label = new Label("Search criteria:") {
+ tooltip =
+ GUI.tooltip_lines(
+ "Search criteria for find operation, e.g.\n\"_ = _\" \"op +\" name: Group -name: monoid")
+ }
+
+ val query = make_query("isabelle-find-theorems", query_label.tooltip, apply_query _)
+
+
+ /* controls */
+
+ private val limit = new TextField(PIDE.options.int("find_theorems_limit").toString, 5) {
+ tooltip = "Limit of displayed results"
+ verifier = (s: String) =>
+ s match { case Properties.Value.Int(x) => x >= 0 case _ => false }
+ listenTo(keys)
+ reactions += { case KeyPressed(_, Key.Enter, 0, _) => apply_query() }
+ }
+
+ private val allow_dups = new CheckBox("Duplicates") {
+ tooltip = "Show all versions of matching theorems"
+ selected = false
+ }
+
+ private val apply_button = new Button("Apply") {
+ tooltip = "Find theorems meeting specified criteria"
+ reactions += { case ButtonClicked(_) => apply_query() }
+ }
+
+
+ /* GUI page */
+
+ private val controls: List[Component] =
+ List(query_label, Component.wrap(query), limit, allow_dups,
+ process_indicator.component, apply_button, zoom)
+
+ val page =
+ new TabbedPane.Page("Theorems", new BorderPanel {
+ add(new Wrap_Panel(Wrap_Panel.Alignment.Right)(controls:_*), BorderPanel.Position.North)
+ add(Component.wrap(pretty_text_area), BorderPanel.Position.Center)
+ }, apply_button.tooltip)
+ }
+
+
+ /* operations */
+
+ private val operations = List(find_theorems)
+
+ private val tabs = new TabbedPane { for (op <- operations) pages += op.page }
+ set_content(tabs)
+
+ override def focusOnDefaultComponent {
+ try { operations(tabs.selection.index).query.requestFocus }
+ catch { case _: IndexOutOfBoundsException => }
+ }
/* resize */
- private var zoom_factor = 100
-
- private def handle_resize()
- {
- Swing_Thread.require {}
-
- pretty_text_area.resize(
- Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
- }
+ private def handle_resize(): Unit =
+ Swing_Thread.require {
+ for (op <- operations) {
+ op.pretty_text_area.resize(
+ Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
+ }
+ }
private val delay_resize =
Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
@@ -77,69 +181,14 @@
{
PIDE.session.global_options += main
handle_resize()
- find_theorems.activate()
+ operations.foreach(op => op.query_operation.activate())
}
override def exit()
{
- find_theorems.deactivate()
+ operations.foreach(op => op.query_operation.deactivate())
PIDE.session.global_options -= main
delay_resize.revoke()
}
-
-
- /* controls */
-
- private def clicked
- {
- find_theorems.apply_query(List(limit.text, allow_dups.selected.toString, query.getText))
- }
-
- private val query_label = new Label("Search criteria:") {
- tooltip =
- GUI.tooltip_lines(
- "Search criteria for find operation, e.g.\n\"_ = _\" \"op +\" name: Group -name: monoid")
- }
-
- private val query = new Completion_Popup.History_Text_Field("isabelle-find-theorems") {
- override def processKeyEvent(evt: KeyEvent)
- {
- if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER) clicked
- super.processKeyEvent(evt)
- }
- { val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) }
- setColumns(40)
- setToolTipText(query_label.tooltip)
- setFont(GUI.imitate_font(Font_Info.main_family(), getFont, 1.2))
- }
+}
- private val limit = new TextField(PIDE.options.int("find_theorems_limit").toString, 5) {
- tooltip = "Limit of displayed results"
- verifier = (s: String) =>
- s match { case Properties.Value.Int(x) => x >= 0 case _ => false }
- listenTo(keys)
- reactions += { case KeyPressed(_, Key.Enter, 0, _) => clicked }
- }
-
- private val allow_dups = new CheckBox("Duplicates") {
- tooltip = "Show all versions of matching theorems"
- selected = false
- }
-
- private val apply_query = new Button("Apply") {
- tooltip = "Find theorems meeting specified criteria"
- reactions += { case ButtonClicked(_) => clicked }
- }
-
- private val zoom = new GUI.Zoom_Box(factor => { zoom_factor = factor; handle_resize() }) {
- tooltip = "Zoom factor for output font size"
- }
-
- private val controls =
- new Wrap_Panel(Wrap_Panel.Alignment.Right)(
- query_label, Component.wrap(query), limit, allow_dups,
- process_indicator.component, apply_query, zoom)
- add(controls.peer, BorderLayout.NORTH)
-
- override def focusOnDefaultComponent { query.requestFocus }
-}