1.1 --- a/NEWS Tue May 06 16:41:24 2014 +0200
1.2 +++ b/NEWS Tue May 06 16:57:17 2014 +0200
1.3 @@ -112,8 +112,10 @@
1.4 * Document panel: simplied interaction where every single mouse click
1.5 (re)opens document via desktop environment or as jEdit buffer.
1.6
1.7 -* Find panel: support for 'find_consts' in addition to
1.8 -'find_theorems'.
1.9 +* More general "Query" panel supersedes "Find" panel, with GUI access
1.10 +to commands 'find_theorems' and 'find_consts', as well as print
1.11 +operations for the context. Minor incompatibility in keyboard
1.12 +shortcuts etc.: replace action isabelle-find by isabelle-query.
1.13
1.14 * Option "jedit_print_mode" (see also "Plugin Options / Isabelle /
1.15 General") allows to specify additional print modes for the prover
2.1 --- a/src/Tools/jEdit/lib/Tools/jedit Tue May 06 16:41:24 2014 +0200
2.2 +++ b/src/Tools/jEdit/lib/Tools/jedit Tue May 06 16:57:17 2014 +0200
2.3 @@ -15,7 +15,6 @@
2.4 "src/document_model.scala"
2.5 "src/document_view.scala"
2.6 "src/documentation_dockable.scala"
2.7 - "src/find_dockable.scala"
2.8 "src/fold_handling.scala"
2.9 "src/font_info.scala"
2.10 "src/graphview_dockable.scala"
2.11 @@ -36,6 +35,7 @@
2.12 "src/pretty_tooltip.scala"
2.13 "src/process_indicator.scala"
2.14 "src/protocol_dockable.scala"
2.15 + "src/query_dockable.scala"
2.16 "src/raw_output_dockable.scala"
2.17 "src/rendering.scala"
2.18 "src/rich_text_area.scala"
3.1 --- a/src/Tools/jEdit/src/Isabelle.props Tue May 06 16:41:24 2014 +0200
3.2 +++ b/src/Tools/jEdit/src/Isabelle.props Tue May 06 16:57:17 2014 +0200
3.3 @@ -31,10 +31,10 @@
3.4 plugin.isabelle.jedit.Plugin.menu.label=Isabelle
3.5 plugin.isabelle.jedit.Plugin.menu= \
3.6 isabelle-documentation \
3.7 - isabelle-find \
3.8 isabelle-monitor \
3.9 isabelle-output \
3.10 isabelle-protocol \
3.11 + isabelle-query \
3.12 isabelle-raw-output \
3.13 isabelle-simplifier-trace \
3.14 isabelle-sledgehammer \
3.15 @@ -44,8 +44,6 @@
3.16 isabelle-timing
3.17 isabelle-documentation.label=Documentation panel
3.18 isabelle-documentation.title=Documentation
3.19 -isabelle-find.label=Find panel
3.20 -isabelle-find.title=Find
3.21 isabelle-graphview.label=Graphview panel
3.22 isabelle-graphview.title=Graphview
3.23 isabelle-info.label=Info panel
3.24 @@ -56,6 +54,8 @@
3.25 isabelle-output.title=Output
3.26 isabelle-protocol.label=Protocol panel
3.27 isabelle-protocol.title=Protocol
3.28 +isabelle-query.label=Query panel
3.29 +isabelle-query.title=Query
3.30 isabelle-raw-output.label=Raw Output panel
3.31 isabelle-raw-output.title=Raw Output
3.32 isabelle-simplifier-trace.label=Simplifier Trace panel
4.1 --- a/src/Tools/jEdit/src/dockables.xml Tue May 06 16:41:24 2014 +0200
4.2 +++ b/src/Tools/jEdit/src/dockables.xml Tue May 06 16:57:17 2014 +0200
4.3 @@ -5,9 +5,6 @@
4.4 <DOCKABLE NAME="isabelle-documentation" MOVABLE="TRUE">
4.5 new isabelle.jedit.Documentation_Dockable(view, position);
4.6 </DOCKABLE>
4.7 - <DOCKABLE NAME="isabelle-find" MOVABLE="TRUE">
4.8 - new isabelle.jedit.Find_Dockable(view, position);
4.9 - </DOCKABLE>
4.10 <DOCKABLE NAME="isabelle-info" MOVABLE="TRUE">
4.11 new isabelle.jedit.Info_Dockable(view, position);
4.12 </DOCKABLE>
4.13 @@ -23,6 +20,9 @@
4.14 <DOCKABLE NAME="isabelle-protocol" MOVABLE="TRUE">
4.15 new isabelle.jedit.Protocol_Dockable(view, position);
4.16 </DOCKABLE>
4.17 + <DOCKABLE NAME="isabelle-query" MOVABLE="TRUE">
4.18 + new isabelle.jedit.Query_Dockable(view, position);
4.19 + </DOCKABLE>
4.20 <DOCKABLE NAME="isabelle-raw-output" MOVABLE="TRUE">
4.21 new isabelle.jedit.Raw_Output_Dockable(view, position);
4.22 </DOCKABLE>
5.1 --- a/src/Tools/jEdit/src/find_dockable.scala Tue May 06 16:41:24 2014 +0200
5.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
5.3 @@ -1,336 +0,0 @@
5.4 -/* Title: Tools/jEdit/src/find_dockable.scala
5.5 - Author: Makarius
5.6 -
5.7 -Dockable window for "find" dialog.
5.8 -*/
5.9 -
5.10 -package isabelle.jedit
5.11 -
5.12 -
5.13 -import isabelle._
5.14 -
5.15 -import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent}
5.16 -import javax.swing.{JComponent, JTextField}
5.17 -
5.18 -import scala.swing.{Button, Component, TextField, CheckBox, Label, ListView,
5.19 - ComboBox, TabbedPane, BorderPanel}
5.20 -import scala.swing.event.{SelectionChanged, ButtonClicked, Key, KeyPressed}
5.21 -
5.22 -import org.gjt.sp.jedit.View
5.23 -
5.24 -
5.25 -object Find_Dockable
5.26 -{
5.27 - private abstract class Operation(view: View)
5.28 - {
5.29 - val pretty_text_area = new Pretty_Text_Area(view)
5.30 - def query_operation: Query_Operation[View]
5.31 - def query: JComponent
5.32 - def select: Unit
5.33 - def page: TabbedPane.Page
5.34 - }
5.35 -}
5.36 -
5.37 -class Find_Dockable(view: View, position: String) extends Dockable(view, position)
5.38 -{
5.39 - /* common GUI components */
5.40 -
5.41 - private var zoom_factor = 100
5.42 -
5.43 - private val zoom =
5.44 - new GUI.Zoom_Box(factor => if (zoom_factor != factor) { zoom_factor = factor; handle_resize() })
5.45 - {
5.46 - tooltip = "Zoom factor for output font size"
5.47 - }
5.48 -
5.49 -
5.50 - private def make_query(property: String, tooltip: String, apply_query: () => Unit): JTextField =
5.51 - new Completion_Popup.History_Text_Field(property)
5.52 - {
5.53 - override def processKeyEvent(evt: KeyEvent)
5.54 - {
5.55 - if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER) apply_query()
5.56 - super.processKeyEvent(evt)
5.57 - }
5.58 - { val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) }
5.59 - setColumns(40)
5.60 - setToolTipText(tooltip)
5.61 - setFont(GUI.imitate_font(Font_Info.main_family(), getFont, 1.2))
5.62 - }
5.63 -
5.64 -
5.65 - /* consume status */
5.66 -
5.67 - def consume_status(process_indicator: Process_Indicator, status: Query_Operation.Status.Value)
5.68 - {
5.69 - status match {
5.70 - case Query_Operation.Status.WAITING =>
5.71 - process_indicator.update("Waiting for evaluation of context ...", 5)
5.72 - case Query_Operation.Status.RUNNING =>
5.73 - process_indicator.update("Running find operation ...", 15)
5.74 - case Query_Operation.Status.FINISHED =>
5.75 - process_indicator.update(null, 0)
5.76 - }
5.77 - }
5.78 -
5.79 -
5.80 - /* find theorems */
5.81 -
5.82 - private val find_theorems = new Find_Dockable.Operation(view)
5.83 - {
5.84 - /* query */
5.85 -
5.86 - private val process_indicator = new Process_Indicator
5.87 -
5.88 - val query_operation =
5.89 - new Query_Operation(PIDE.editor, view, "find_theorems",
5.90 - consume_status(process_indicator, _),
5.91 - (snapshot, results, body) =>
5.92 - pretty_text_area.update(snapshot, results, Pretty.separate(body)))
5.93 -
5.94 - private def apply_query()
5.95 - {
5.96 - query_operation.apply_query(List(limit.text, allow_dups.selected.toString, query.getText))
5.97 - }
5.98 -
5.99 - private val query_label = new Label("Search criteria:") {
5.100 - tooltip =
5.101 - GUI.tooltip_lines(
5.102 - "Search criteria for find operation, e.g.\n\"_ = _\" \"op +\" name: Group -name: monoid")
5.103 - }
5.104 -
5.105 - val query = make_query("isabelle-find-theorems", query_label.tooltip, apply_query _)
5.106 -
5.107 -
5.108 - /* GUI page */
5.109 -
5.110 - private val limit = new TextField(PIDE.options.int("find_theorems_limit").toString, 5) {
5.111 - tooltip = "Limit of displayed results"
5.112 - verifier = (s: String) =>
5.113 - s match { case Properties.Value.Int(x) => x >= 0 case _ => false }
5.114 - listenTo(keys)
5.115 - reactions += { case KeyPressed(_, Key.Enter, 0, _) => apply_query() }
5.116 - }
5.117 -
5.118 - private val allow_dups = new CheckBox("Duplicates") {
5.119 - tooltip = "Show all versions of matching theorems"
5.120 - selected = false
5.121 - }
5.122 -
5.123 - private val apply_button = new Button("Apply") {
5.124 - tooltip = "Find theorems meeting specified criteria"
5.125 - reactions += { case ButtonClicked(_) => apply_query() }
5.126 - }
5.127 -
5.128 - private val control_panel =
5.129 - new Wrap_Panel(Wrap_Panel.Alignment.Right)(
5.130 - query_label, Component.wrap(query), limit, allow_dups,
5.131 - process_indicator.component, apply_button)
5.132 -
5.133 - def select { control_panel.contents += zoom }
5.134 -
5.135 - val page =
5.136 - new TabbedPane.Page("Theorems", new BorderPanel {
5.137 - add(control_panel, BorderPanel.Position.North)
5.138 - add(Component.wrap(pretty_text_area), BorderPanel.Position.Center)
5.139 - }, apply_button.tooltip)
5.140 - }
5.141 -
5.142 -
5.143 - /* find consts */
5.144 -
5.145 - private val find_consts = new Find_Dockable.Operation(view)
5.146 - {
5.147 - /* query */
5.148 -
5.149 - private val process_indicator = new Process_Indicator
5.150 -
5.151 - val query_operation =
5.152 - new Query_Operation(PIDE.editor, view, "find_consts",
5.153 - consume_status(process_indicator, _),
5.154 - (snapshot, results, body) =>
5.155 - pretty_text_area.update(snapshot, results, Pretty.separate(body)))
5.156 -
5.157 - private def apply_query()
5.158 - {
5.159 - query_operation.apply_query(List(query.getText))
5.160 - }
5.161 -
5.162 - private val query_label = new Label("Search criteria:") {
5.163 - tooltip = GUI.tooltip_lines("Name / type patterns for constants")
5.164 - }
5.165 -
5.166 - val query = make_query("isabelle-find-consts", query_label.tooltip, apply_query _)
5.167 -
5.168 -
5.169 - /* GUI page */
5.170 -
5.171 - private val apply_button = new Button("Apply") {
5.172 - tooltip = "Find constants by name / type patterns"
5.173 - reactions += { case ButtonClicked(_) => apply_query() }
5.174 - }
5.175 -
5.176 - private val control_panel =
5.177 - new Wrap_Panel(Wrap_Panel.Alignment.Right)(
5.178 - query_label, Component.wrap(query), process_indicator.component, apply_button)
5.179 -
5.180 - def select { control_panel.contents += zoom }
5.181 -
5.182 - val page =
5.183 - new TabbedPane.Page("Constants", new BorderPanel {
5.184 - add(control_panel, BorderPanel.Position.North)
5.185 - add(Component.wrap(pretty_text_area), BorderPanel.Position.Center)
5.186 - }, apply_button.tooltip)
5.187 - }
5.188 -
5.189 -
5.190 - /* print operation */
5.191 -
5.192 - private val print_operation = new Find_Dockable.Operation(view)
5.193 - {
5.194 - /* query */
5.195 -
5.196 - val query_operation =
5.197 - new Query_Operation(PIDE.editor, view, "print_operation", _ => (),
5.198 - (snapshot, results, body) =>
5.199 - pretty_text_area.update(snapshot, results, Pretty.separate(body)))
5.200 -
5.201 - private def apply_query()
5.202 - {
5.203 - query_operation.apply_query(List(_selector.selection.item))
5.204 - }
5.205 -
5.206 - private val query_label = new Label("Print:")
5.207 -
5.208 - def query: JComponent = _selector.peer.asInstanceOf[JComponent]
5.209 -
5.210 -
5.211 - /* items */
5.212 -
5.213 - case class Item(name: String, description: String)
5.214 -
5.215 - class Renderer(old_renderer: ListView.Renderer[String], items: List[Item])
5.216 - extends ListView.Renderer[String]
5.217 - {
5.218 - def componentFor(list: ListView[_],
5.219 - selected: Boolean, focused: Boolean, item: String, index: Int) =
5.220 - {
5.221 - val component = old_renderer.componentFor(list, selected, focused, item, index)
5.222 - try { component.tooltip = items(index).description }
5.223 - catch { case _: IndexOutOfBoundsException => }
5.224 - component
5.225 - }
5.226 - }
5.227 -
5.228 - private var _selector_item: Option[String] = None
5.229 - private var _selector = new ComboBox[String](Nil)
5.230 -
5.231 - private def set_selector()
5.232 - {
5.233 - val items = Print_Operation.print_operations(PIDE.session).map(p => Item(p._1, p._2))
5.234 -
5.235 - _selector =
5.236 - new ComboBox(items.map(_.name)) {
5.237 - _selector_item.foreach(item => selection.item = item)
5.238 - listenTo(selection)
5.239 - reactions += {
5.240 - case SelectionChanged(_) =>
5.241 - _selector_item = Some(selection.item)
5.242 - apply_query()
5.243 - }
5.244 - }
5.245 - _selector.renderer = new Renderer(_selector.renderer, items)
5.246 - }
5.247 - set_selector()
5.248 -
5.249 -
5.250 - /* GUI page */
5.251 -
5.252 - private val apply_button = new Button("Apply") {
5.253 - tooltip = "Apply to current context"
5.254 - reactions += { case ButtonClicked(_) => apply_query() }
5.255 - }
5.256 -
5.257 - private val control_panel = new Wrap_Panel(Wrap_Panel.Alignment.Right)()
5.258 -
5.259 - def select
5.260 - {
5.261 - set_selector()
5.262 - control_panel.contents.clear
5.263 - control_panel.contents ++= List(query_label, _selector, apply_button, zoom)
5.264 - }
5.265 -
5.266 - val page =
5.267 - new TabbedPane.Page("Print ...", new BorderPanel {
5.268 - add(control_panel, BorderPanel.Position.North)
5.269 - add(Component.wrap(pretty_text_area), BorderPanel.Position.Center)
5.270 - }, "Print information from context")
5.271 - }
5.272 -
5.273 -
5.274 - /* operations */
5.275 -
5.276 - private val operations = List(find_theorems, find_consts, print_operation)
5.277 -
5.278 - private val operations_pane = new TabbedPane
5.279 - {
5.280 - pages ++= operations.map(_.page)
5.281 - listenTo(selection)
5.282 - reactions += { case SelectionChanged(_) => select_operation() }
5.283 - }
5.284 -
5.285 - private def get_operation(): Option[Find_Dockable.Operation] =
5.286 - try { Some(operations(operations_pane.selection.index)) }
5.287 - catch { case _: IndexOutOfBoundsException => None }
5.288 -
5.289 - private def select_operation() {
5.290 - for (op <- get_operation()) { op.select; op.query.requestFocus }
5.291 - operations_pane.revalidate
5.292 - }
5.293 -
5.294 - override def focusOnDefaultComponent { for (op <- get_operation()) op.query.requestFocus }
5.295 -
5.296 - select_operation()
5.297 - set_content(operations_pane)
5.298 -
5.299 -
5.300 - /* resize */
5.301 -
5.302 - private def handle_resize(): Unit =
5.303 - Swing_Thread.require {
5.304 - for (op <- operations) {
5.305 - op.pretty_text_area.resize(
5.306 - Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
5.307 - }
5.308 - }
5.309 -
5.310 - private val delay_resize =
5.311 - Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
5.312 -
5.313 - addComponentListener(new ComponentAdapter {
5.314 - override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
5.315 - })
5.316 -
5.317 -
5.318 - /* main */
5.319 -
5.320 - private val main =
5.321 - Session.Consumer[Session.Global_Options](getClass.getName) {
5.322 - case _: Session.Global_Options => Swing_Thread.later { handle_resize() }
5.323 - }
5.324 -
5.325 - override def init()
5.326 - {
5.327 - PIDE.session.global_options += main
5.328 - handle_resize()
5.329 - operations.foreach(op => op.query_operation.activate())
5.330 - }
5.331 -
5.332 - override def exit()
5.333 - {
5.334 - operations.foreach(op => op.query_operation.deactivate())
5.335 - PIDE.session.global_options -= main
5.336 - delay_resize.revoke()
5.337 - }
5.338 -}
5.339 -
6.1 --- a/src/Tools/jEdit/src/isabelle.scala Tue May 06 16:41:24 2014 +0200
6.2 +++ b/src/Tools/jEdit/src/isabelle.scala Tue May 06 16:57:17 2014 +0200
6.3 @@ -78,12 +78,6 @@
6.4 case _ => None
6.5 }
6.6
6.7 - def find_dockable(view: View): Option[Find_Dockable] =
6.8 - wm(view).getDockableWindow("isabelle-find") match {
6.9 - case dockable: Find_Dockable => Some(dockable)
6.10 - case _ => None
6.11 - }
6.12 -
6.13 def monitor_dockable(view: View): Option[Monitor_Dockable] =
6.14 wm(view).getDockableWindow("isabelle-monitor") match {
6.15 case dockable: Monitor_Dockable => Some(dockable)
6.16 @@ -102,6 +96,12 @@
6.17 case _ => None
6.18 }
6.19
6.20 + def query_dockable(view: View): Option[Query_Dockable] =
6.21 + wm(view).getDockableWindow("isabelle-query") match {
6.22 + case dockable: Query_Dockable => Some(dockable)
6.23 + case _ => None
6.24 + }
6.25 +
6.26 def raw_output_dockable(view: View): Option[Raw_Output_Dockable] =
6.27 wm(view).getDockableWindow("isabelle-raw-output") match {
6.28 case dockable: Raw_Output_Dockable => Some(dockable)
7.1 --- a/src/Tools/jEdit/src/jEdit.props Tue May 06 16:41:24 2014 +0200
7.2 +++ b/src/Tools/jEdit/src/jEdit.props Tue May 06 16:57:17 2014 +0200
7.3 @@ -184,10 +184,10 @@
7.4 insert-newline-indent.shortcut=
7.5 insert-newline.shortcut=ENTER
7.6 isabelle-documentation.dock-position=right
7.7 -isabelle-find.dock-position=bottom
7.8 isabelle-output.dock-position=bottom
7.9 isabelle-output.height=174
7.10 isabelle-output.width=412
7.11 +isabelle-query.dock-position=bottom
7.12 isabelle-simplifier-trace.dock-position=bottom
7.13 isabelle-sledgehammer.dock-position=bottom
7.14 isabelle-symbols.dock-position=bottom
8.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
8.2 +++ b/src/Tools/jEdit/src/query_dockable.scala Tue May 06 16:57:17 2014 +0200
8.3 @@ -0,0 +1,336 @@
8.4 +/* Title: Tools/jEdit/src/query_dockable.scala
8.5 + Author: Makarius
8.6 +
8.7 +Dockable window for query operations.
8.8 +*/
8.9 +
8.10 +package isabelle.jedit
8.11 +
8.12 +
8.13 +import isabelle._
8.14 +
8.15 +import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent}
8.16 +import javax.swing.{JComponent, JTextField}
8.17 +
8.18 +import scala.swing.{Button, Component, TextField, CheckBox, Label, ListView,
8.19 + ComboBox, TabbedPane, BorderPanel}
8.20 +import scala.swing.event.{SelectionChanged, ButtonClicked, Key, KeyPressed}
8.21 +
8.22 +import org.gjt.sp.jedit.View
8.23 +
8.24 +
8.25 +object Query_Dockable
8.26 +{
8.27 + private abstract class Operation(view: View)
8.28 + {
8.29 + val pretty_text_area = new Pretty_Text_Area(view)
8.30 + def query_operation: Query_Operation[View]
8.31 + def query: JComponent
8.32 + def select: Unit
8.33 + def page: TabbedPane.Page
8.34 + }
8.35 +}
8.36 +
8.37 +class Query_Dockable(view: View, position: String) extends Dockable(view, position)
8.38 +{
8.39 + /* common GUI components */
8.40 +
8.41 + private var zoom_factor = 100
8.42 +
8.43 + private val zoom =
8.44 + new GUI.Zoom_Box(factor => if (zoom_factor != factor) { zoom_factor = factor; handle_resize() })
8.45 + {
8.46 + tooltip = "Zoom factor for output font size"
8.47 + }
8.48 +
8.49 +
8.50 + private def make_query(property: String, tooltip: String, apply_query: () => Unit): JTextField =
8.51 + new Completion_Popup.History_Text_Field(property)
8.52 + {
8.53 + override def processKeyEvent(evt: KeyEvent)
8.54 + {
8.55 + if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER) apply_query()
8.56 + super.processKeyEvent(evt)
8.57 + }
8.58 + { val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) }
8.59 + setColumns(40)
8.60 + setToolTipText(tooltip)
8.61 + setFont(GUI.imitate_font(Font_Info.main_family(), getFont, 1.2))
8.62 + }
8.63 +
8.64 +
8.65 + /* consume status */
8.66 +
8.67 + def consume_status(process_indicator: Process_Indicator, status: Query_Operation.Status.Value)
8.68 + {
8.69 + status match {
8.70 + case Query_Operation.Status.WAITING =>
8.71 + process_indicator.update("Waiting for evaluation of context ...", 5)
8.72 + case Query_Operation.Status.RUNNING =>
8.73 + process_indicator.update("Running find operation ...", 15)
8.74 + case Query_Operation.Status.FINISHED =>
8.75 + process_indicator.update(null, 0)
8.76 + }
8.77 + }
8.78 +
8.79 +
8.80 + /* find theorems */
8.81 +
8.82 + private val find_theorems = new Query_Dockable.Operation(view)
8.83 + {
8.84 + /* query */
8.85 +
8.86 + private val process_indicator = new Process_Indicator
8.87 +
8.88 + val query_operation =
8.89 + new Query_Operation(PIDE.editor, view, "find_theorems",
8.90 + consume_status(process_indicator, _),
8.91 + (snapshot, results, body) =>
8.92 + pretty_text_area.update(snapshot, results, Pretty.separate(body)))
8.93 +
8.94 + private def apply_query()
8.95 + {
8.96 + query_operation.apply_query(List(limit.text, allow_dups.selected.toString, query.getText))
8.97 + }
8.98 +
8.99 + private val query_label = new Label("Search criteria:") {
8.100 + tooltip =
8.101 + GUI.tooltip_lines(
8.102 + "Search criteria for find operation, e.g.\n\"_ = _\" \"op +\" name: Group -name: monoid")
8.103 + }
8.104 +
8.105 + val query = make_query("isabelle-find-theorems", query_label.tooltip, apply_query _)
8.106 +
8.107 +
8.108 + /* GUI page */
8.109 +
8.110 + private val limit = new TextField(PIDE.options.int("find_theorems_limit").toString, 5) {
8.111 + tooltip = "Limit of displayed results"
8.112 + verifier = (s: String) =>
8.113 + s match { case Properties.Value.Int(x) => x >= 0 case _ => false }
8.114 + listenTo(keys)
8.115 + reactions += { case KeyPressed(_, Key.Enter, 0, _) => apply_query() }
8.116 + }
8.117 +
8.118 + private val allow_dups = new CheckBox("Duplicates") {
8.119 + tooltip = "Show all versions of matching theorems"
8.120 + selected = false
8.121 + }
8.122 +
8.123 + private val apply_button = new Button("Apply") {
8.124 + tooltip = "Find theorems meeting specified criteria"
8.125 + reactions += { case ButtonClicked(_) => apply_query() }
8.126 + }
8.127 +
8.128 + private val control_panel =
8.129 + new Wrap_Panel(Wrap_Panel.Alignment.Right)(
8.130 + query_label, Component.wrap(query), limit, allow_dups,
8.131 + process_indicator.component, apply_button)
8.132 +
8.133 + def select { control_panel.contents += zoom }
8.134 +
8.135 + val page =
8.136 + new TabbedPane.Page("Find Theorems", new BorderPanel {
8.137 + add(control_panel, BorderPanel.Position.North)
8.138 + add(Component.wrap(pretty_text_area), BorderPanel.Position.Center)
8.139 + }, apply_button.tooltip)
8.140 + }
8.141 +
8.142 +
8.143 + /* find consts */
8.144 +
8.145 + private val find_consts = new Query_Dockable.Operation(view)
8.146 + {
8.147 + /* query */
8.148 +
8.149 + private val process_indicator = new Process_Indicator
8.150 +
8.151 + val query_operation =
8.152 + new Query_Operation(PIDE.editor, view, "find_consts",
8.153 + consume_status(process_indicator, _),
8.154 + (snapshot, results, body) =>
8.155 + pretty_text_area.update(snapshot, results, Pretty.separate(body)))
8.156 +
8.157 + private def apply_query()
8.158 + {
8.159 + query_operation.apply_query(List(query.getText))
8.160 + }
8.161 +
8.162 + private val query_label = new Label("Search criteria:") {
8.163 + tooltip = GUI.tooltip_lines("Name / type patterns for constants")
8.164 + }
8.165 +
8.166 + val query = make_query("isabelle-find-consts", query_label.tooltip, apply_query _)
8.167 +
8.168 +
8.169 + /* GUI page */
8.170 +
8.171 + private val apply_button = new Button("Apply") {
8.172 + tooltip = "Find constants by name / type patterns"
8.173 + reactions += { case ButtonClicked(_) => apply_query() }
8.174 + }
8.175 +
8.176 + private val control_panel =
8.177 + new Wrap_Panel(Wrap_Panel.Alignment.Right)(
8.178 + query_label, Component.wrap(query), process_indicator.component, apply_button)
8.179 +
8.180 + def select { control_panel.contents += zoom }
8.181 +
8.182 + val page =
8.183 + new TabbedPane.Page("Find Constants", new BorderPanel {
8.184 + add(control_panel, BorderPanel.Position.North)
8.185 + add(Component.wrap(pretty_text_area), BorderPanel.Position.Center)
8.186 + }, apply_button.tooltip)
8.187 + }
8.188 +
8.189 +
8.190 + /* print operation */
8.191 +
8.192 + private val print_operation = new Query_Dockable.Operation(view)
8.193 + {
8.194 + /* query */
8.195 +
8.196 + val query_operation =
8.197 + new Query_Operation(PIDE.editor, view, "print_operation", _ => (),
8.198 + (snapshot, results, body) =>
8.199 + pretty_text_area.update(snapshot, results, Pretty.separate(body)))
8.200 +
8.201 + private def apply_query()
8.202 + {
8.203 + query_operation.apply_query(List(_selector.selection.item))
8.204 + }
8.205 +
8.206 + private val query_label = new Label("Print:")
8.207 +
8.208 + def query: JComponent = _selector.peer.asInstanceOf[JComponent]
8.209 +
8.210 +
8.211 + /* items */
8.212 +
8.213 + case class Item(name: String, description: String)
8.214 +
8.215 + class Renderer(old_renderer: ListView.Renderer[String], items: List[Item])
8.216 + extends ListView.Renderer[String]
8.217 + {
8.218 + def componentFor(list: ListView[_],
8.219 + selected: Boolean, focused: Boolean, item: String, index: Int) =
8.220 + {
8.221 + val component = old_renderer.componentFor(list, selected, focused, item, index)
8.222 + try { component.tooltip = items(index).description }
8.223 + catch { case _: IndexOutOfBoundsException => }
8.224 + component
8.225 + }
8.226 + }
8.227 +
8.228 + private var _selector_item: Option[String] = None
8.229 + private var _selector = new ComboBox[String](Nil)
8.230 +
8.231 + private def set_selector()
8.232 + {
8.233 + val items = Print_Operation.print_operations(PIDE.session).map(p => Item(p._1, p._2))
8.234 +
8.235 + _selector =
8.236 + new ComboBox(items.map(_.name)) {
8.237 + _selector_item.foreach(item => selection.item = item)
8.238 + listenTo(selection)
8.239 + reactions += {
8.240 + case SelectionChanged(_) =>
8.241 + _selector_item = Some(selection.item)
8.242 + apply_query()
8.243 + }
8.244 + }
8.245 + _selector.renderer = new Renderer(_selector.renderer, items)
8.246 + }
8.247 + set_selector()
8.248 +
8.249 +
8.250 + /* GUI page */
8.251 +
8.252 + private val apply_button = new Button("Apply") {
8.253 + tooltip = "Apply to current context"
8.254 + reactions += { case ButtonClicked(_) => apply_query() }
8.255 + }
8.256 +
8.257 + private val control_panel = new Wrap_Panel(Wrap_Panel.Alignment.Right)()
8.258 +
8.259 + def select
8.260 + {
8.261 + set_selector()
8.262 + control_panel.contents.clear
8.263 + control_panel.contents ++= List(query_label, _selector, apply_button, zoom)
8.264 + }
8.265 +
8.266 + val page =
8.267 + new TabbedPane.Page("Print Context", new BorderPanel {
8.268 + add(control_panel, BorderPanel.Position.North)
8.269 + add(Component.wrap(pretty_text_area), BorderPanel.Position.Center)
8.270 + }, "Print information from context")
8.271 + }
8.272 +
8.273 +
8.274 + /* operations */
8.275 +
8.276 + private val operations = List(find_theorems, find_consts, print_operation)
8.277 +
8.278 + private val operations_pane = new TabbedPane
8.279 + {
8.280 + pages ++= operations.map(_.page)
8.281 + listenTo(selection)
8.282 + reactions += { case SelectionChanged(_) => select_operation() }
8.283 + }
8.284 +
8.285 + private def get_operation(): Option[Query_Dockable.Operation] =
8.286 + try { Some(operations(operations_pane.selection.index)) }
8.287 + catch { case _: IndexOutOfBoundsException => None }
8.288 +
8.289 + private def select_operation() {
8.290 + for (op <- get_operation()) { op.select; op.query.requestFocus }
8.291 + operations_pane.revalidate
8.292 + }
8.293 +
8.294 + override def focusOnDefaultComponent { for (op <- get_operation()) op.query.requestFocus }
8.295 +
8.296 + select_operation()
8.297 + set_content(operations_pane)
8.298 +
8.299 +
8.300 + /* resize */
8.301 +
8.302 + private def handle_resize(): Unit =
8.303 + Swing_Thread.require {
8.304 + for (op <- operations) {
8.305 + op.pretty_text_area.resize(
8.306 + Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
8.307 + }
8.308 + }
8.309 +
8.310 + private val delay_resize =
8.311 + Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
8.312 +
8.313 + addComponentListener(new ComponentAdapter {
8.314 + override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
8.315 + })
8.316 +
8.317 +
8.318 + /* main */
8.319 +
8.320 + private val main =
8.321 + Session.Consumer[Session.Global_Options](getClass.getName) {
8.322 + case _: Session.Global_Options => Swing_Thread.later { handle_resize() }
8.323 + }
8.324 +
8.325 + override def init()
8.326 + {
8.327 + PIDE.session.global_options += main
8.328 + handle_resize()
8.329 + operations.foreach(op => op.query_operation.activate())
8.330 + }
8.331 +
8.332 + override def exit()
8.333 + {
8.334 + operations.foreach(op => op.query_operation.deactivate())
8.335 + PIDE.session.global_options -= main
8.336 + delay_resize.revoke()
8.337 + }
8.338 +}
8.339 +