# HG changeset patch # User wenzelm # Date 1398539810 -7200 # Node ID d6fdf08282f39d9e3d84c3fd5a25587e84c24892 # Parent a18c76b7b299c74e989b84a3c4a2b26562aed5d3 some rearrangements to support multiple find operations; diff -r a18c76b7b299 -r d6fdf08282f3 src/Tools/jEdit/src/find_dockable.scala --- 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 } -}