src/Tools/jEdit/src/query_dockable.scala
author wenzelm
Thu May 08 11:47:38 2014 +0200 (2014-05-08)
changeset 56907 0f3c375fd27c
parent 56906 408b526911f7
child 56909 a1557dc7f589
permissions -rw-r--r--
enable "PIDE" docking framework by default, and rely on its "Detach" menu item;
wenzelm@56879
     1
/*  Title:      Tools/jEdit/src/query_dockable.scala
wenzelm@52846
     2
    Author:     Makarius
wenzelm@52846
     3
wenzelm@56879
     4
Dockable window for query operations.
wenzelm@52846
     5
*/
wenzelm@52846
     6
wenzelm@52846
     7
package isabelle.jedit
wenzelm@52846
     8
wenzelm@52846
     9
wenzelm@52846
    10
import isabelle._
wenzelm@52846
    11
wenzelm@56757
    12
import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent}
wenzelm@56757
    13
import javax.swing.{JComponent, JTextField}
wenzelm@52846
    14
wenzelm@56872
    15
import scala.swing.{Button, Component, TextField, CheckBox, Label, ListView,
wenzelm@56757
    16
  ComboBox, TabbedPane, BorderPanel}
wenzelm@56759
    17
import scala.swing.event.{SelectionChanged, ButtonClicked, Key, KeyPressed}
wenzelm@52846
    18
wenzelm@52846
    19
import org.gjt.sp.jedit.View
wenzelm@52846
    20
wenzelm@52846
    21
wenzelm@56879
    22
object Query_Dockable
wenzelm@56757
    23
{
wenzelm@56758
    24
  private abstract class Operation(view: View)
wenzelm@56757
    25
  {
wenzelm@56758
    26
    val pretty_text_area = new Pretty_Text_Area(view)
wenzelm@56757
    27
    def query_operation: Query_Operation[View]
wenzelm@56757
    28
    def query: JComponent
wenzelm@56759
    29
    def select: Unit
wenzelm@56757
    30
    def page: TabbedPane.Page
wenzelm@56757
    31
  }
wenzelm@56757
    32
}
wenzelm@56757
    33
wenzelm@56879
    34
class Query_Dockable(view: View, position: String) extends Dockable(view, position)
wenzelm@52846
    35
{
wenzelm@56757
    36
  /* common GUI components */
wenzelm@56757
    37
wenzelm@56757
    38
  private var zoom_factor = 100
wenzelm@56757
    39
  private val zoom =
wenzelm@56757
    40
    new GUI.Zoom_Box(factor => if (zoom_factor != factor) { zoom_factor = factor; handle_resize() })
wenzelm@56757
    41
    {
wenzelm@56757
    42
      tooltip = "Zoom factor for output font size"
wenzelm@56757
    43
    }
wenzelm@52846
    44
wenzelm@56757
    45
  private def make_query(property: String, tooltip: String, apply_query: () => Unit): JTextField =
wenzelm@56757
    46
    new Completion_Popup.History_Text_Field(property)
wenzelm@56757
    47
    {
wenzelm@56757
    48
      override def processKeyEvent(evt: KeyEvent)
wenzelm@56757
    49
      {
wenzelm@56757
    50
        if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER) apply_query()
wenzelm@56757
    51
        super.processKeyEvent(evt)
wenzelm@56757
    52
      }
wenzelm@56757
    53
      { val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) }
wenzelm@56757
    54
      setColumns(40)
wenzelm@56757
    55
      setToolTipText(tooltip)
wenzelm@56757
    56
      setFont(GUI.imitate_font(Font_Info.main_family(), getFont, 1.2))
wenzelm@56757
    57
    }
wenzelm@52865
    58
wenzelm@52935
    59
wenzelm@56757
    60
  /* consume status */
wenzelm@56757
    61
wenzelm@56757
    62
  def consume_status(process_indicator: Process_Indicator, status: Query_Operation.Status.Value)
wenzelm@52935
    63
  {
wenzelm@52935
    64
    status match {
wenzelm@52935
    65
      case Query_Operation.Status.WAITING =>
wenzelm@52935
    66
        process_indicator.update("Waiting for evaluation of context ...", 5)
wenzelm@52935
    67
      case Query_Operation.Status.RUNNING =>
wenzelm@52935
    68
        process_indicator.update("Running find operation ...", 15)
wenzelm@54640
    69
      case Query_Operation.Status.FINISHED =>
wenzelm@52935
    70
        process_indicator.update(null, 0)
wenzelm@52935
    71
    }
wenzelm@52935
    72
  }
wenzelm@52935
    73
wenzelm@56757
    74
wenzelm@56757
    75
  /* find theorems */
wenzelm@56757
    76
wenzelm@56879
    77
  private val find_theorems = new Query_Dockable.Operation(view)
wenzelm@56757
    78
  {
wenzelm@56757
    79
    /* query */
wenzelm@56757
    80
wenzelm@56757
    81
    private val process_indicator = new Process_Indicator
wenzelm@56757
    82
wenzelm@56757
    83
    val query_operation =
wenzelm@56757
    84
      new Query_Operation(PIDE.editor, view, "find_theorems",
wenzelm@56757
    85
        consume_status(process_indicator, _),
wenzelm@56757
    86
        (snapshot, results, body) =>
wenzelm@56757
    87
          pretty_text_area.update(snapshot, results, Pretty.separate(body)))
wenzelm@56757
    88
wenzelm@56757
    89
    private def apply_query()
wenzelm@56757
    90
    {
wenzelm@56757
    91
      query_operation.apply_query(List(limit.text, allow_dups.selected.toString, query.getText))
wenzelm@56757
    92
    }
wenzelm@56757
    93
wenzelm@56883
    94
    private val query_label = new Label("Query:") {
wenzelm@56757
    95
      tooltip =
wenzelm@56757
    96
        GUI.tooltip_lines(
wenzelm@56757
    97
          "Search criteria for find operation, e.g.\n\"_ = _\" \"op +\" name: Group -name: monoid")
wenzelm@56757
    98
    }
wenzelm@56757
    99
wenzelm@56757
   100
    val query = make_query("isabelle-find-theorems", query_label.tooltip, apply_query _)
wenzelm@56757
   101
wenzelm@56757
   102
wenzelm@56758
   103
    /* GUI page */
wenzelm@56757
   104
wenzelm@56757
   105
    private val limit = new TextField(PIDE.options.int("find_theorems_limit").toString, 5) {
wenzelm@56757
   106
      tooltip = "Limit of displayed results"
wenzelm@56757
   107
      verifier = (s: String) =>
wenzelm@56757
   108
        s match { case Properties.Value.Int(x) => x >= 0 case _ => false }
wenzelm@56757
   109
      listenTo(keys)
wenzelm@56757
   110
      reactions += { case KeyPressed(_, Key.Enter, 0, _) => apply_query() }
wenzelm@56757
   111
    }
wenzelm@56757
   112
wenzelm@56757
   113
    private val allow_dups = new CheckBox("Duplicates") {
wenzelm@56757
   114
      tooltip = "Show all versions of matching theorems"
wenzelm@56757
   115
      selected = false
wenzelm@56757
   116
    }
wenzelm@56757
   117
wenzelm@56757
   118
    private val apply_button = new Button("Apply") {
wenzelm@56757
   119
      tooltip = "Find theorems meeting specified criteria"
wenzelm@56757
   120
      reactions += { case ButtonClicked(_) => apply_query() }
wenzelm@56757
   121
    }
wenzelm@56757
   122
wenzelm@56759
   123
    private val control_panel =
wenzelm@56759
   124
      new Wrap_Panel(Wrap_Panel.Alignment.Right)(
wenzelm@56759
   125
        query_label, Component.wrap(query), limit, allow_dups,
wenzelm@56907
   126
        process_indicator.component, apply_button,
wenzelm@56886
   127
        pretty_text_area.search_label, pretty_text_area.search_pattern)
wenzelm@56759
   128
wenzelm@56759
   129
    def select { control_panel.contents += zoom }
wenzelm@56757
   130
wenzelm@56757
   131
    val page =
wenzelm@56879
   132
      new TabbedPane.Page("Find Theorems", new BorderPanel {
wenzelm@56759
   133
        add(control_panel, BorderPanel.Position.North)
wenzelm@56757
   134
        add(Component.wrap(pretty_text_area), BorderPanel.Position.Center)
wenzelm@56757
   135
      }, apply_button.tooltip)
wenzelm@56757
   136
  }
wenzelm@56757
   137
wenzelm@56757
   138
wenzelm@56758
   139
  /* find consts */
wenzelm@56758
   140
wenzelm@56879
   141
  private val find_consts = new Query_Dockable.Operation(view)
wenzelm@56758
   142
  {
wenzelm@56758
   143
    /* query */
wenzelm@56758
   144
wenzelm@56758
   145
    private val process_indicator = new Process_Indicator
wenzelm@56758
   146
wenzelm@56758
   147
    val query_operation =
wenzelm@56758
   148
      new Query_Operation(PIDE.editor, view, "find_consts",
wenzelm@56758
   149
        consume_status(process_indicator, _),
wenzelm@56758
   150
        (snapshot, results, body) =>
wenzelm@56758
   151
          pretty_text_area.update(snapshot, results, Pretty.separate(body)))
wenzelm@56758
   152
wenzelm@56758
   153
    private def apply_query()
wenzelm@56758
   154
    {
wenzelm@56758
   155
      query_operation.apply_query(List(query.getText))
wenzelm@56758
   156
    }
wenzelm@56758
   157
wenzelm@56883
   158
    private val query_label = new Label("Query:") {
wenzelm@56758
   159
      tooltip = GUI.tooltip_lines("Name / type patterns for constants")
wenzelm@56758
   160
    }
wenzelm@56758
   161
wenzelm@56758
   162
    val query = make_query("isabelle-find-consts", query_label.tooltip, apply_query _)
wenzelm@56758
   163
wenzelm@56758
   164
wenzelm@56758
   165
    /* GUI page */
wenzelm@56758
   166
wenzelm@56758
   167
    private val apply_button = new Button("Apply") {
wenzelm@56758
   168
      tooltip = "Find constants by name / type patterns"
wenzelm@56758
   169
      reactions += { case ButtonClicked(_) => apply_query() }
wenzelm@56758
   170
    }
wenzelm@56758
   171
wenzelm@56759
   172
    private val control_panel =
wenzelm@56759
   173
      new Wrap_Panel(Wrap_Panel.Alignment.Right)(
wenzelm@56907
   174
        query_label, Component.wrap(query), process_indicator.component, apply_button,
wenzelm@56886
   175
        pretty_text_area.search_label, pretty_text_area.search_pattern)
wenzelm@56759
   176
wenzelm@56759
   177
    def select { control_panel.contents += zoom }
wenzelm@56758
   178
wenzelm@56758
   179
    val page =
wenzelm@56879
   180
      new TabbedPane.Page("Find Constants", new BorderPanel {
wenzelm@56759
   181
        add(control_panel, BorderPanel.Position.North)
wenzelm@56758
   182
        add(Component.wrap(pretty_text_area), BorderPanel.Position.Center)
wenzelm@56758
   183
      }, apply_button.tooltip)
wenzelm@56758
   184
  }
wenzelm@56758
   185
wenzelm@56758
   186
wenzelm@56864
   187
  /* print operation */
wenzelm@56864
   188
wenzelm@56879
   189
  private val print_operation = new Query_Dockable.Operation(view)
wenzelm@56864
   190
  {
wenzelm@56864
   191
    /* query */
wenzelm@56864
   192
wenzelm@56864
   193
    val query_operation =
wenzelm@56864
   194
      new Query_Operation(PIDE.editor, view, "print_operation", _ => (),
wenzelm@56864
   195
        (snapshot, results, body) =>
wenzelm@56864
   196
          pretty_text_area.update(snapshot, results, Pretty.separate(body)))
wenzelm@56864
   197
wenzelm@56864
   198
    private def apply_query()
wenzelm@56864
   199
    {
wenzelm@56882
   200
      query_operation.apply_query(List(selector.selection.item))
wenzelm@56864
   201
    }
wenzelm@56864
   202
wenzelm@56866
   203
    private val query_label = new Label("Print:")
wenzelm@56882
   204
    def query: JComponent = apply_button.peer
wenzelm@56864
   205
wenzelm@56864
   206
wenzelm@56872
   207
    /* items */
wenzelm@56864
   208
wenzelm@56872
   209
    case class Item(name: String, description: String)
wenzelm@56872
   210
wenzelm@56872
   211
    class Renderer(old_renderer: ListView.Renderer[String], items: List[Item])
wenzelm@56872
   212
      extends ListView.Renderer[String]
wenzelm@56864
   213
    {
wenzelm@56872
   214
      def componentFor(list: ListView[_],
wenzelm@56872
   215
        selected: Boolean, focused: Boolean, item: String, index: Int) =
wenzelm@56872
   216
      {
wenzelm@56872
   217
        val component = old_renderer.componentFor(list, selected, focused, item, index)
wenzelm@56872
   218
        try { component.tooltip = items(index).description }
wenzelm@56872
   219
        catch { case _: IndexOutOfBoundsException => }
wenzelm@56872
   220
        component
wenzelm@56872
   221
      }
wenzelm@56872
   222
    }
wenzelm@56872
   223
wenzelm@56882
   224
    private var selector_item: Option[String] = None
wenzelm@56882
   225
    private var selector = new ComboBox[String](Nil)
wenzelm@56872
   226
wenzelm@56872
   227
    private def set_selector()
wenzelm@56872
   228
    {
wenzelm@56872
   229
      val items = Print_Operation.print_operations(PIDE.session).map(p => Item(p._1, p._2))
wenzelm@56872
   230
wenzelm@56882
   231
      selector =
wenzelm@56872
   232
        new ComboBox(items.map(_.name)) {
wenzelm@56882
   233
          selector_item.foreach(item => selection.item = item)
wenzelm@56864
   234
          listenTo(selection)
wenzelm@56864
   235
          reactions += {
wenzelm@56864
   236
            case SelectionChanged(_) =>
wenzelm@56882
   237
              selector_item = Some(selection.item)
wenzelm@56864
   238
              apply_query()
wenzelm@56864
   239
          }
wenzelm@56864
   240
        }
wenzelm@56882
   241
      selector.renderer = new Renderer(selector.renderer, items)
wenzelm@56864
   242
    }
wenzelm@56872
   243
    set_selector()
wenzelm@56872
   244
wenzelm@56872
   245
wenzelm@56872
   246
    /* GUI page */
wenzelm@56864
   247
wenzelm@56865
   248
    private val apply_button = new Button("Apply") {
wenzelm@56865
   249
      tooltip = "Apply to current context"
wenzelm@56865
   250
      reactions += { case ButtonClicked(_) => apply_query() }
wenzelm@56865
   251
    }
wenzelm@56865
   252
wenzelm@56864
   253
    private val control_panel = new Wrap_Panel(Wrap_Panel.Alignment.Right)()
wenzelm@56864
   254
wenzelm@56864
   255
    def select
wenzelm@56864
   256
    {
wenzelm@56872
   257
      set_selector()
wenzelm@56864
   258
      control_panel.contents.clear
wenzelm@56883
   259
      control_panel.contents ++=
wenzelm@56907
   260
        List(query_label, selector, apply_button,
wenzelm@56886
   261
          pretty_text_area.search_label, pretty_text_area.search_pattern, zoom)
wenzelm@56864
   262
    }
wenzelm@56864
   263
wenzelm@56864
   264
    val page =
wenzelm@56879
   265
      new TabbedPane.Page("Print Context", new BorderPanel {
wenzelm@56864
   266
        add(control_panel, BorderPanel.Position.North)
wenzelm@56864
   267
        add(Component.wrap(pretty_text_area), BorderPanel.Position.Center)
wenzelm@56864
   268
      }, "Print information from context")
wenzelm@56864
   269
  }
wenzelm@56864
   270
wenzelm@56864
   271
wenzelm@56757
   272
  /* operations */
wenzelm@56757
   273
wenzelm@56864
   274
  private val operations = List(find_theorems, find_consts, print_operation)
wenzelm@56757
   275
wenzelm@56759
   276
  private val operations_pane = new TabbedPane
wenzelm@56759
   277
  {
wenzelm@56759
   278
    pages ++= operations.map(_.page)
wenzelm@56759
   279
    listenTo(selection)
wenzelm@56759
   280
    reactions += { case SelectionChanged(_) => select_operation() }
wenzelm@56759
   281
  }
wenzelm@56757
   282
wenzelm@56879
   283
  private def get_operation(): Option[Query_Dockable.Operation] =
wenzelm@56759
   284
    try { Some(operations(operations_pane.selection.index)) }
wenzelm@56759
   285
    catch { case _: IndexOutOfBoundsException => None }
wenzelm@56759
   286
wenzelm@56759
   287
  private def select_operation() {
wenzelm@56865
   288
    for (op <- get_operation()) { op.select; op.query.requestFocus }
wenzelm@56759
   289
    operations_pane.revalidate
wenzelm@56757
   290
  }
wenzelm@52865
   291
wenzelm@56759
   292
  override def focusOnDefaultComponent { for (op <- get_operation()) op.query.requestFocus }
wenzelm@56759
   293
wenzelm@56759
   294
  select_operation()
wenzelm@56759
   295
  set_content(operations_pane)
wenzelm@56759
   296
wenzelm@56906
   297
  override val detach_operation = Some(() => get_operation().foreach(_.pretty_text_area.detach))
wenzelm@56906
   298
wenzelm@52865
   299
wenzelm@52865
   300
  /* resize */
wenzelm@52865
   301
wenzelm@56757
   302
  private def handle_resize(): Unit =
wenzelm@56757
   303
    Swing_Thread.require {
wenzelm@56757
   304
      for (op <- operations) {
wenzelm@56757
   305
        op.pretty_text_area.resize(
wenzelm@56757
   306
          Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
wenzelm@56757
   307
      }
wenzelm@56757
   308
    }
wenzelm@52846
   309
wenzelm@52865
   310
  private val delay_resize =
wenzelm@52865
   311
    Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
wenzelm@52854
   312
wenzelm@52865
   313
  addComponentListener(new ComponentAdapter {
wenzelm@52865
   314
    override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
wenzelm@52865
   315
  })
wenzelm@52846
   316
wenzelm@52846
   317
wenzelm@56715
   318
  /* main */
wenzelm@52846
   319
wenzelm@56715
   320
  private val main =
wenzelm@56715
   321
    Session.Consumer[Session.Global_Options](getClass.getName) {
wenzelm@56715
   322
      case _: Session.Global_Options => Swing_Thread.later { handle_resize() }
wenzelm@52846
   323
    }
wenzelm@52846
   324
wenzelm@52846
   325
  override def init()
wenzelm@52846
   326
  {
wenzelm@56715
   327
    PIDE.session.global_options += main
wenzelm@52848
   328
    handle_resize()
wenzelm@56757
   329
    operations.foreach(op => op.query_operation.activate())
wenzelm@52846
   330
  }
wenzelm@52846
   331
wenzelm@52846
   332
  override def exit()
wenzelm@52846
   333
  {
wenzelm@56757
   334
    operations.foreach(op => op.query_operation.deactivate())
wenzelm@56715
   335
    PIDE.session.global_options -= main
wenzelm@52846
   336
    delay_resize.revoke()
wenzelm@52846
   337
  }
wenzelm@56757
   338
}
wenzelm@52846
   339