# HG changeset patch
# User wenzelm
# Date 1399388237 -7200
# Node ID ee2b61f37ad92848af8c3f046a9001ff3149ca59
# Parent a5d082a851248dbef4ae82125ba251d2099c2479
renamed "Find" to "Query", with more general operations;
diff -r a5d082a85124 -r ee2b61f37ad9 NEWS
--- a/NEWS Tue May 06 16:41:24 2014 +0200
+++ b/NEWS Tue May 06 16:57:17 2014 +0200
@@ -112,8 +112,10 @@
* Document panel: simplied interaction where every single mouse click
(re)opens document via desktop environment or as jEdit buffer.
-* Find panel: support for 'find_consts' in addition to
-'find_theorems'.
+* More general "Query" panel supersedes "Find" panel, with GUI access
+to commands 'find_theorems' and 'find_consts', as well as print
+operations for the context. Minor incompatibility in keyboard
+shortcuts etc.: replace action isabelle-find by isabelle-query.
* Option "jedit_print_mode" (see also "Plugin Options / Isabelle /
General") allows to specify additional print modes for the prover
diff -r a5d082a85124 -r ee2b61f37ad9 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit Tue May 06 16:41:24 2014 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Tue May 06 16:57:17 2014 +0200
@@ -15,7 +15,6 @@
"src/document_model.scala"
"src/document_view.scala"
"src/documentation_dockable.scala"
- "src/find_dockable.scala"
"src/fold_handling.scala"
"src/font_info.scala"
"src/graphview_dockable.scala"
@@ -36,6 +35,7 @@
"src/pretty_tooltip.scala"
"src/process_indicator.scala"
"src/protocol_dockable.scala"
+ "src/query_dockable.scala"
"src/raw_output_dockable.scala"
"src/rendering.scala"
"src/rich_text_area.scala"
diff -r a5d082a85124 -r ee2b61f37ad9 src/Tools/jEdit/src/Isabelle.props
--- a/src/Tools/jEdit/src/Isabelle.props Tue May 06 16:41:24 2014 +0200
+++ b/src/Tools/jEdit/src/Isabelle.props Tue May 06 16:57:17 2014 +0200
@@ -31,10 +31,10 @@
plugin.isabelle.jedit.Plugin.menu.label=Isabelle
plugin.isabelle.jedit.Plugin.menu= \
isabelle-documentation \
- isabelle-find \
isabelle-monitor \
isabelle-output \
isabelle-protocol \
+ isabelle-query \
isabelle-raw-output \
isabelle-simplifier-trace \
isabelle-sledgehammer \
@@ -44,8 +44,6 @@
isabelle-timing
isabelle-documentation.label=Documentation panel
isabelle-documentation.title=Documentation
-isabelle-find.label=Find panel
-isabelle-find.title=Find
isabelle-graphview.label=Graphview panel
isabelle-graphview.title=Graphview
isabelle-info.label=Info panel
@@ -56,6 +54,8 @@
isabelle-output.title=Output
isabelle-protocol.label=Protocol panel
isabelle-protocol.title=Protocol
+isabelle-query.label=Query panel
+isabelle-query.title=Query
isabelle-raw-output.label=Raw Output panel
isabelle-raw-output.title=Raw Output
isabelle-simplifier-trace.label=Simplifier Trace panel
diff -r a5d082a85124 -r ee2b61f37ad9 src/Tools/jEdit/src/dockables.xml
--- a/src/Tools/jEdit/src/dockables.xml Tue May 06 16:41:24 2014 +0200
+++ b/src/Tools/jEdit/src/dockables.xml Tue May 06 16:57:17 2014 +0200
@@ -5,9 +5,6 @@
new isabelle.jedit.Documentation_Dockable(view, position);
-
- new isabelle.jedit.Find_Dockable(view, position);
-
new isabelle.jedit.Info_Dockable(view, position);
@@ -23,6 +20,9 @@
new isabelle.jedit.Protocol_Dockable(view, position);
+
+ new isabelle.jedit.Query_Dockable(view, position);
+
new isabelle.jedit.Raw_Output_Dockable(view, position);
diff -r a5d082a85124 -r ee2b61f37ad9 src/Tools/jEdit/src/find_dockable.scala
--- a/src/Tools/jEdit/src/find_dockable.scala Tue May 06 16:41:24 2014 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,336 +0,0 @@
-/* Title: Tools/jEdit/src/find_dockable.scala
- Author: Makarius
-
-Dockable window for "find" dialog.
-*/
-
-package isabelle.jedit
-
-
-import isabelle._
-
-import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent}
-import javax.swing.{JComponent, JTextField}
-
-import scala.swing.{Button, Component, TextField, CheckBox, Label, ListView,
- ComboBox, TabbedPane, BorderPanel}
-import scala.swing.event.{SelectionChanged, ButtonClicked, Key, KeyPressed}
-
-import org.gjt.sp.jedit.View
-
-
-object Find_Dockable
-{
- private abstract class Operation(view: View)
- {
- val pretty_text_area = new Pretty_Text_Area(view)
- def query_operation: Query_Operation[View]
- def query: JComponent
- def select: Unit
- def page: TabbedPane.Page
- }
-}
-
-class Find_Dockable(view: View, position: String) extends Dockable(view, position)
-{
- /* 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"
- }
-
-
- 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))
- }
-
-
- /* consume status */
-
- def consume_status(process_indicator: Process_Indicator, status: Query_Operation.Status.Value)
- {
- status match {
- case Query_Operation.Status.WAITING =>
- process_indicator.update("Waiting for evaluation of context ...", 5)
- case Query_Operation.Status.RUNNING =>
- process_indicator.update("Running find operation ...", 15)
- case Query_Operation.Status.FINISHED =>
- process_indicator.update(null, 0)
- }
- }
-
-
- /* find theorems */
-
- private val find_theorems = new Find_Dockable.Operation(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 _)
-
-
- /* GUI page */
-
- 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() }
- }
-
- private val control_panel =
- new Wrap_Panel(Wrap_Panel.Alignment.Right)(
- query_label, Component.wrap(query), limit, allow_dups,
- process_indicator.component, apply_button)
-
- def select { control_panel.contents += zoom }
-
- val page =
- new TabbedPane.Page("Theorems", new BorderPanel {
- add(control_panel, BorderPanel.Position.North)
- add(Component.wrap(pretty_text_area), BorderPanel.Position.Center)
- }, apply_button.tooltip)
- }
-
-
- /* find consts */
-
- private val find_consts = new Find_Dockable.Operation(view)
- {
- /* query */
-
- private val process_indicator = new Process_Indicator
-
- val query_operation =
- new Query_Operation(PIDE.editor, view, "find_consts",
- 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(query.getText))
- }
-
- private val query_label = new Label("Search criteria:") {
- tooltip = GUI.tooltip_lines("Name / type patterns for constants")
- }
-
- val query = make_query("isabelle-find-consts", query_label.tooltip, apply_query _)
-
-
- /* GUI page */
-
- private val apply_button = new Button("Apply") {
- tooltip = "Find constants by name / type patterns"
- reactions += { case ButtonClicked(_) => apply_query() }
- }
-
- private val control_panel =
- new Wrap_Panel(Wrap_Panel.Alignment.Right)(
- query_label, Component.wrap(query), process_indicator.component, apply_button)
-
- def select { control_panel.contents += zoom }
-
- val page =
- new TabbedPane.Page("Constants", new BorderPanel {
- add(control_panel, BorderPanel.Position.North)
- add(Component.wrap(pretty_text_area), BorderPanel.Position.Center)
- }, apply_button.tooltip)
- }
-
-
- /* print operation */
-
- private val print_operation = new Find_Dockable.Operation(view)
- {
- /* query */
-
- val query_operation =
- new Query_Operation(PIDE.editor, view, "print_operation", _ => (),
- (snapshot, results, body) =>
- pretty_text_area.update(snapshot, results, Pretty.separate(body)))
-
- private def apply_query()
- {
- query_operation.apply_query(List(_selector.selection.item))
- }
-
- private val query_label = new Label("Print:")
-
- def query: JComponent = _selector.peer.asInstanceOf[JComponent]
-
-
- /* items */
-
- case class Item(name: String, description: String)
-
- class Renderer(old_renderer: ListView.Renderer[String], items: List[Item])
- extends ListView.Renderer[String]
- {
- def componentFor(list: ListView[_],
- selected: Boolean, focused: Boolean, item: String, index: Int) =
- {
- val component = old_renderer.componentFor(list, selected, focused, item, index)
- try { component.tooltip = items(index).description }
- catch { case _: IndexOutOfBoundsException => }
- component
- }
- }
-
- private var _selector_item: Option[String] = None
- private var _selector = new ComboBox[String](Nil)
-
- private def set_selector()
- {
- val items = Print_Operation.print_operations(PIDE.session).map(p => Item(p._1, p._2))
-
- _selector =
- new ComboBox(items.map(_.name)) {
- _selector_item.foreach(item => selection.item = item)
- listenTo(selection)
- reactions += {
- case SelectionChanged(_) =>
- _selector_item = Some(selection.item)
- apply_query()
- }
- }
- _selector.renderer = new Renderer(_selector.renderer, items)
- }
- set_selector()
-
-
- /* GUI page */
-
- private val apply_button = new Button("Apply") {
- tooltip = "Apply to current context"
- reactions += { case ButtonClicked(_) => apply_query() }
- }
-
- private val control_panel = new Wrap_Panel(Wrap_Panel.Alignment.Right)()
-
- def select
- {
- set_selector()
- control_panel.contents.clear
- control_panel.contents ++= List(query_label, _selector, apply_button, zoom)
- }
-
- val page =
- new TabbedPane.Page("Print ...", new BorderPanel {
- add(control_panel, BorderPanel.Position.North)
- add(Component.wrap(pretty_text_area), BorderPanel.Position.Center)
- }, "Print information from context")
- }
-
-
- /* operations */
-
- private val operations = List(find_theorems, find_consts, print_operation)
-
- private val operations_pane = new TabbedPane
- {
- pages ++= operations.map(_.page)
- listenTo(selection)
- reactions += { case SelectionChanged(_) => select_operation() }
- }
-
- private def get_operation(): Option[Find_Dockable.Operation] =
- try { Some(operations(operations_pane.selection.index)) }
- catch { case _: IndexOutOfBoundsException => None }
-
- private def select_operation() {
- for (op <- get_operation()) { op.select; op.query.requestFocus }
- operations_pane.revalidate
- }
-
- override def focusOnDefaultComponent { for (op <- get_operation()) op.query.requestFocus }
-
- select_operation()
- set_content(operations_pane)
-
-
- /* resize */
-
- 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() }
-
- addComponentListener(new ComponentAdapter {
- override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
- })
-
-
- /* main */
-
- private val main =
- Session.Consumer[Session.Global_Options](getClass.getName) {
- case _: Session.Global_Options => Swing_Thread.later { handle_resize() }
- }
-
- override def init()
- {
- PIDE.session.global_options += main
- handle_resize()
- operations.foreach(op => op.query_operation.activate())
- }
-
- override def exit()
- {
- operations.foreach(op => op.query_operation.deactivate())
- PIDE.session.global_options -= main
- delay_resize.revoke()
- }
-}
-
diff -r a5d082a85124 -r ee2b61f37ad9 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala Tue May 06 16:41:24 2014 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala Tue May 06 16:57:17 2014 +0200
@@ -78,12 +78,6 @@
case _ => None
}
- def find_dockable(view: View): Option[Find_Dockable] =
- wm(view).getDockableWindow("isabelle-find") match {
- case dockable: Find_Dockable => Some(dockable)
- case _ => None
- }
-
def monitor_dockable(view: View): Option[Monitor_Dockable] =
wm(view).getDockableWindow("isabelle-monitor") match {
case dockable: Monitor_Dockable => Some(dockable)
@@ -102,6 +96,12 @@
case _ => None
}
+ def query_dockable(view: View): Option[Query_Dockable] =
+ wm(view).getDockableWindow("isabelle-query") match {
+ case dockable: Query_Dockable => Some(dockable)
+ case _ => None
+ }
+
def raw_output_dockable(view: View): Option[Raw_Output_Dockable] =
wm(view).getDockableWindow("isabelle-raw-output") match {
case dockable: Raw_Output_Dockable => Some(dockable)
diff -r a5d082a85124 -r ee2b61f37ad9 src/Tools/jEdit/src/jEdit.props
--- a/src/Tools/jEdit/src/jEdit.props Tue May 06 16:41:24 2014 +0200
+++ b/src/Tools/jEdit/src/jEdit.props Tue May 06 16:57:17 2014 +0200
@@ -184,10 +184,10 @@
insert-newline-indent.shortcut=
insert-newline.shortcut=ENTER
isabelle-documentation.dock-position=right
-isabelle-find.dock-position=bottom
isabelle-output.dock-position=bottom
isabelle-output.height=174
isabelle-output.width=412
+isabelle-query.dock-position=bottom
isabelle-simplifier-trace.dock-position=bottom
isabelle-sledgehammer.dock-position=bottom
isabelle-symbols.dock-position=bottom
diff -r a5d082a85124 -r ee2b61f37ad9 src/Tools/jEdit/src/query_dockable.scala
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/query_dockable.scala Tue May 06 16:57:17 2014 +0200
@@ -0,0 +1,336 @@
+/* Title: Tools/jEdit/src/query_dockable.scala
+ Author: Makarius
+
+Dockable window for query operations.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent}
+import javax.swing.{JComponent, JTextField}
+
+import scala.swing.{Button, Component, TextField, CheckBox, Label, ListView,
+ ComboBox, TabbedPane, BorderPanel}
+import scala.swing.event.{SelectionChanged, ButtonClicked, Key, KeyPressed}
+
+import org.gjt.sp.jedit.View
+
+
+object Query_Dockable
+{
+ private abstract class Operation(view: View)
+ {
+ val pretty_text_area = new Pretty_Text_Area(view)
+ def query_operation: Query_Operation[View]
+ def query: JComponent
+ def select: Unit
+ def page: TabbedPane.Page
+ }
+}
+
+class Query_Dockable(view: View, position: String) extends Dockable(view, position)
+{
+ /* 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"
+ }
+
+
+ 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))
+ }
+
+
+ /* consume status */
+
+ def consume_status(process_indicator: Process_Indicator, status: Query_Operation.Status.Value)
+ {
+ status match {
+ case Query_Operation.Status.WAITING =>
+ process_indicator.update("Waiting for evaluation of context ...", 5)
+ case Query_Operation.Status.RUNNING =>
+ process_indicator.update("Running find operation ...", 15)
+ case Query_Operation.Status.FINISHED =>
+ process_indicator.update(null, 0)
+ }
+ }
+
+
+ /* find theorems */
+
+ private val find_theorems = new Query_Dockable.Operation(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 _)
+
+
+ /* GUI page */
+
+ 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() }
+ }
+
+ private val control_panel =
+ new Wrap_Panel(Wrap_Panel.Alignment.Right)(
+ query_label, Component.wrap(query), limit, allow_dups,
+ process_indicator.component, apply_button)
+
+ def select { control_panel.contents += zoom }
+
+ val page =
+ new TabbedPane.Page("Find Theorems", new BorderPanel {
+ add(control_panel, BorderPanel.Position.North)
+ add(Component.wrap(pretty_text_area), BorderPanel.Position.Center)
+ }, apply_button.tooltip)
+ }
+
+
+ /* find consts */
+
+ private val find_consts = new Query_Dockable.Operation(view)
+ {
+ /* query */
+
+ private val process_indicator = new Process_Indicator
+
+ val query_operation =
+ new Query_Operation(PIDE.editor, view, "find_consts",
+ 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(query.getText))
+ }
+
+ private val query_label = new Label("Search criteria:") {
+ tooltip = GUI.tooltip_lines("Name / type patterns for constants")
+ }
+
+ val query = make_query("isabelle-find-consts", query_label.tooltip, apply_query _)
+
+
+ /* GUI page */
+
+ private val apply_button = new Button("Apply") {
+ tooltip = "Find constants by name / type patterns"
+ reactions += { case ButtonClicked(_) => apply_query() }
+ }
+
+ private val control_panel =
+ new Wrap_Panel(Wrap_Panel.Alignment.Right)(
+ query_label, Component.wrap(query), process_indicator.component, apply_button)
+
+ def select { control_panel.contents += zoom }
+
+ val page =
+ new TabbedPane.Page("Find Constants", new BorderPanel {
+ add(control_panel, BorderPanel.Position.North)
+ add(Component.wrap(pretty_text_area), BorderPanel.Position.Center)
+ }, apply_button.tooltip)
+ }
+
+
+ /* print operation */
+
+ private val print_operation = new Query_Dockable.Operation(view)
+ {
+ /* query */
+
+ val query_operation =
+ new Query_Operation(PIDE.editor, view, "print_operation", _ => (),
+ (snapshot, results, body) =>
+ pretty_text_area.update(snapshot, results, Pretty.separate(body)))
+
+ private def apply_query()
+ {
+ query_operation.apply_query(List(_selector.selection.item))
+ }
+
+ private val query_label = new Label("Print:")
+
+ def query: JComponent = _selector.peer.asInstanceOf[JComponent]
+
+
+ /* items */
+
+ case class Item(name: String, description: String)
+
+ class Renderer(old_renderer: ListView.Renderer[String], items: List[Item])
+ extends ListView.Renderer[String]
+ {
+ def componentFor(list: ListView[_],
+ selected: Boolean, focused: Boolean, item: String, index: Int) =
+ {
+ val component = old_renderer.componentFor(list, selected, focused, item, index)
+ try { component.tooltip = items(index).description }
+ catch { case _: IndexOutOfBoundsException => }
+ component
+ }
+ }
+
+ private var _selector_item: Option[String] = None
+ private var _selector = new ComboBox[String](Nil)
+
+ private def set_selector()
+ {
+ val items = Print_Operation.print_operations(PIDE.session).map(p => Item(p._1, p._2))
+
+ _selector =
+ new ComboBox(items.map(_.name)) {
+ _selector_item.foreach(item => selection.item = item)
+ listenTo(selection)
+ reactions += {
+ case SelectionChanged(_) =>
+ _selector_item = Some(selection.item)
+ apply_query()
+ }
+ }
+ _selector.renderer = new Renderer(_selector.renderer, items)
+ }
+ set_selector()
+
+
+ /* GUI page */
+
+ private val apply_button = new Button("Apply") {
+ tooltip = "Apply to current context"
+ reactions += { case ButtonClicked(_) => apply_query() }
+ }
+
+ private val control_panel = new Wrap_Panel(Wrap_Panel.Alignment.Right)()
+
+ def select
+ {
+ set_selector()
+ control_panel.contents.clear
+ control_panel.contents ++= List(query_label, _selector, apply_button, zoom)
+ }
+
+ val page =
+ new TabbedPane.Page("Print Context", new BorderPanel {
+ add(control_panel, BorderPanel.Position.North)
+ add(Component.wrap(pretty_text_area), BorderPanel.Position.Center)
+ }, "Print information from context")
+ }
+
+
+ /* operations */
+
+ private val operations = List(find_theorems, find_consts, print_operation)
+
+ private val operations_pane = new TabbedPane
+ {
+ pages ++= operations.map(_.page)
+ listenTo(selection)
+ reactions += { case SelectionChanged(_) => select_operation() }
+ }
+
+ private def get_operation(): Option[Query_Dockable.Operation] =
+ try { Some(operations(operations_pane.selection.index)) }
+ catch { case _: IndexOutOfBoundsException => None }
+
+ private def select_operation() {
+ for (op <- get_operation()) { op.select; op.query.requestFocus }
+ operations_pane.revalidate
+ }
+
+ override def focusOnDefaultComponent { for (op <- get_operation()) op.query.requestFocus }
+
+ select_operation()
+ set_content(operations_pane)
+
+
+ /* resize */
+
+ 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() }
+
+ addComponentListener(new ComponentAdapter {
+ override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
+ })
+
+
+ /* main */
+
+ private val main =
+ Session.Consumer[Session.Global_Options](getClass.getName) {
+ case _: Session.Global_Options => Swing_Thread.later { handle_resize() }
+ }
+
+ override def init()
+ {
+ PIDE.session.global_options += main
+ handle_resize()
+ operations.foreach(op => op.query_operation.activate())
+ }
+
+ override def exit()
+ {
+ operations.foreach(op => op.query_operation.deactivate())
+ PIDE.session.global_options -= main
+ delay_resize.revoke()
+ }
+}
+