renamed "Find" to "Query", with more general operations;
authorwenzelm
Tue May 06 16:57:17 2014 +0200 (2014-05-06)
changeset 56879ee2b61f37ad9
parent 56878 a5d082a85124
child 56880 f8c1d2583699
renamed "Find" to "Query", with more general operations;
NEWS
src/Tools/jEdit/lib/Tools/jedit
src/Tools/jEdit/src/Isabelle.props
src/Tools/jEdit/src/dockables.xml
src/Tools/jEdit/src/find_dockable.scala
src/Tools/jEdit/src/isabelle.scala
src/Tools/jEdit/src/jEdit.props
src/Tools/jEdit/src/query_dockable.scala
     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 +