src/Tools/jEdit/src/query_dockable.scala
author wenzelm
Mon Jan 09 20:26:59 2017 +0100 (2017-01-09)
changeset 64854 f5aa712e6250
parent 63805 c272680df665
child 65246 848965b5befc
permissions -rw-r--r--
tuned signature;
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@57044
    38
  private val zoom = new Font_Info.Zoom_Box { def changed = handle_resize() }
wenzelm@52846
    39
wenzelm@60861
    40
  private def make_query(property: String, tooltip: String, apply_query: () => Unit)
wenzelm@60861
    41
      : Completion_Popup.History_Text_Field =
wenzelm@56757
    42
    new Completion_Popup.History_Text_Field(property)
wenzelm@56757
    43
    {
wenzelm@56757
    44
      override def processKeyEvent(evt: KeyEvent)
wenzelm@56757
    45
      {
wenzelm@56757
    46
        if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER) apply_query()
wenzelm@56757
    47
        super.processKeyEvent(evt)
wenzelm@56757
    48
      }
wenzelm@56757
    49
      { val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) }
wenzelm@56757
    50
      setColumns(40)
wenzelm@56757
    51
      setToolTipText(tooltip)
wenzelm@59286
    52
      setFont(GUI.imitate_font(getFont, Font_Info.main_family(), 1.2))
wenzelm@56757
    53
    }
wenzelm@52865
    54
wenzelm@52935
    55
wenzelm@56757
    56
  /* consume status */
wenzelm@56757
    57
wenzelm@56757
    58
  def consume_status(process_indicator: Process_Indicator, status: Query_Operation.Status.Value)
wenzelm@52935
    59
  {
wenzelm@52935
    60
    status match {
wenzelm@52935
    61
      case Query_Operation.Status.WAITING =>
wenzelm@52935
    62
        process_indicator.update("Waiting for evaluation of context ...", 5)
wenzelm@52935
    63
      case Query_Operation.Status.RUNNING =>
wenzelm@52935
    64
        process_indicator.update("Running find operation ...", 15)
wenzelm@54640
    65
      case Query_Operation.Status.FINISHED =>
wenzelm@52935
    66
        process_indicator.update(null, 0)
wenzelm@52935
    67
    }
wenzelm@52935
    68
  }
wenzelm@52935
    69
wenzelm@56757
    70
wenzelm@56757
    71
  /* find theorems */
wenzelm@56757
    72
wenzelm@56879
    73
  private val find_theorems = new Query_Dockable.Operation(view)
wenzelm@56757
    74
  {
wenzelm@56757
    75
    /* query */
wenzelm@56757
    76
wenzelm@56757
    77
    private val process_indicator = new Process_Indicator
wenzelm@56757
    78
wenzelm@56757
    79
    val query_operation =
wenzelm@56757
    80
      new Query_Operation(PIDE.editor, view, "find_theorems",
wenzelm@56757
    81
        consume_status(process_indicator, _),
wenzelm@56757
    82
        (snapshot, results, body) =>
wenzelm@56757
    83
          pretty_text_area.update(snapshot, results, Pretty.separate(body)))
wenzelm@56757
    84
wenzelm@56757
    85
    private def apply_query()
wenzelm@56757
    86
    {
wenzelm@60861
    87
      query.addCurrentToHistory()
wenzelm@56757
    88
      query_operation.apply_query(List(limit.text, allow_dups.selected.toString, query.getText))
wenzelm@56757
    89
    }
wenzelm@56757
    90
wenzelm@56909
    91
    private val query_label = new Label("Find:") {
wenzelm@56757
    92
      tooltip =
wenzelm@56757
    93
        GUI.tooltip_lines(
wenzelm@56757
    94
          "Search criteria for find operation, e.g.\n\"_ = _\" \"op +\" name: Group -name: monoid")
wenzelm@56757
    95
    }
wenzelm@56757
    96
wenzelm@56757
    97
    val query = make_query("isabelle-find-theorems", query_label.tooltip, apply_query _)
wenzelm@56757
    98
wenzelm@56757
    99
wenzelm@56758
   100
    /* GUI page */
wenzelm@56757
   101
wenzelm@56757
   102
    private val limit = new TextField(PIDE.options.int("find_theorems_limit").toString, 5) {
wenzelm@56757
   103
      tooltip = "Limit of displayed results"
wenzelm@56757
   104
      verifier = (s: String) =>
wenzelm@63805
   105
        s match { case Value.Int(x) => x >= 0 case _ => false }
wenzelm@56757
   106
      listenTo(keys)
wenzelm@56757
   107
      reactions += { case KeyPressed(_, Key.Enter, 0, _) => apply_query() }
wenzelm@56757
   108
    }
wenzelm@56757
   109
wenzelm@56757
   110
    private val allow_dups = new CheckBox("Duplicates") {
wenzelm@56757
   111
      tooltip = "Show all versions of matching theorems"
wenzelm@56757
   112
      selected = false
wenzelm@56911
   113
      reactions += { case ButtonClicked(_) => apply_query() }
wenzelm@56757
   114
    }
wenzelm@56757
   115
wenzelm@56910
   116
    private val apply_button = new Button("<html><b>Apply</b></html>") {
wenzelm@56757
   117
      tooltip = "Find theorems meeting specified criteria"
wenzelm@56757
   118
      reactions += { case ButtonClicked(_) => apply_query() }
wenzelm@56757
   119
    }
wenzelm@56757
   120
wenzelm@56759
   121
    private val control_panel =
wenzelm@56759
   122
      new Wrap_Panel(Wrap_Panel.Alignment.Right)(
wenzelm@56759
   123
        query_label, Component.wrap(query), limit, allow_dups,
wenzelm@56907
   124
        process_indicator.component, apply_button,
wenzelm@57042
   125
        pretty_text_area.search_label, pretty_text_area.search_field)
wenzelm@56759
   126
wenzelm@56759
   127
    def select { control_panel.contents += zoom }
wenzelm@56757
   128
wenzelm@56757
   129
    val page =
wenzelm@56879
   130
      new TabbedPane.Page("Find Theorems", new BorderPanel {
wenzelm@59391
   131
        layout(control_panel) = BorderPanel.Position.North
wenzelm@59391
   132
        layout(Component.wrap(pretty_text_area)) = BorderPanel.Position.Center
wenzelm@56757
   133
      }, apply_button.tooltip)
wenzelm@56757
   134
  }
wenzelm@56757
   135
wenzelm@56757
   136
wenzelm@56758
   137
  /* find consts */
wenzelm@56758
   138
wenzelm@56879
   139
  private val find_consts = new Query_Dockable.Operation(view)
wenzelm@56758
   140
  {
wenzelm@56758
   141
    /* query */
wenzelm@56758
   142
wenzelm@56758
   143
    private val process_indicator = new Process_Indicator
wenzelm@56758
   144
wenzelm@56758
   145
    val query_operation =
wenzelm@56758
   146
      new Query_Operation(PIDE.editor, view, "find_consts",
wenzelm@56758
   147
        consume_status(process_indicator, _),
wenzelm@56758
   148
        (snapshot, results, body) =>
wenzelm@56758
   149
          pretty_text_area.update(snapshot, results, Pretty.separate(body)))
wenzelm@56758
   150
wenzelm@56758
   151
    private def apply_query()
wenzelm@56758
   152
    {
wenzelm@60861
   153
      query.addCurrentToHistory()
wenzelm@56758
   154
      query_operation.apply_query(List(query.getText))
wenzelm@56758
   155
    }
wenzelm@56758
   156
wenzelm@56909
   157
    private val query_label = new Label("Find:") {
wenzelm@56758
   158
      tooltip = GUI.tooltip_lines("Name / type patterns for constants")
wenzelm@56758
   159
    }
wenzelm@56758
   160
wenzelm@56758
   161
    val query = make_query("isabelle-find-consts", query_label.tooltip, apply_query _)
wenzelm@56758
   162
wenzelm@56758
   163
wenzelm@56758
   164
    /* GUI page */
wenzelm@56758
   165
wenzelm@56910
   166
    private val apply_button = new Button("<html><b>Apply</b></html>") {
wenzelm@56758
   167
      tooltip = "Find constants by name / type patterns"
wenzelm@56758
   168
      reactions += { case ButtonClicked(_) => apply_query() }
wenzelm@56758
   169
    }
wenzelm@56758
   170
wenzelm@56759
   171
    private val control_panel =
wenzelm@56759
   172
      new Wrap_Panel(Wrap_Panel.Alignment.Right)(
wenzelm@56907
   173
        query_label, Component.wrap(query), process_indicator.component, apply_button,
wenzelm@57042
   174
        pretty_text_area.search_label, pretty_text_area.search_field)
wenzelm@56759
   175
wenzelm@56759
   176
    def select { control_panel.contents += zoom }
wenzelm@56758
   177
wenzelm@56758
   178
    val page =
wenzelm@56879
   179
      new TabbedPane.Page("Find Constants", new BorderPanel {
wenzelm@59391
   180
        layout(control_panel) = BorderPanel.Position.North
wenzelm@59391
   181
        layout(Component.wrap(pretty_text_area)) = BorderPanel.Position.Center
wenzelm@56758
   182
      }, apply_button.tooltip)
wenzelm@56758
   183
  }
wenzelm@56758
   184
wenzelm@56758
   185
wenzelm@56864
   186
  /* print operation */
wenzelm@56864
   187
wenzelm@56879
   188
  private val print_operation = new Query_Dockable.Operation(view)
wenzelm@56864
   189
  {
wenzelm@57604
   190
    /* items */
wenzelm@57604
   191
wenzelm@57604
   192
    private class Item(val name: String, description: String, sel: Boolean)
wenzelm@57604
   193
    {
wenzelm@57604
   194
      val checkbox = new CheckBox(name) {
wenzelm@57604
   195
        tooltip = "Print " + description
wenzelm@57604
   196
        selected = sel
wenzelm@57604
   197
        reactions += { case ButtonClicked(_) => apply_query() }
wenzelm@57604
   198
      }
wenzelm@57604
   199
    }
wenzelm@57604
   200
wenzelm@57604
   201
    private var _items: List[Item] = Nil
wenzelm@57604
   202
wenzelm@57604
   203
    private def selected_items(): List[String] =
wenzelm@57604
   204
      for (item <- _items if item.checkbox.selected) yield item.name
wenzelm@57604
   205
wenzelm@57604
   206
    private def update_items(): List[Item] =
wenzelm@57604
   207
    {
wenzelm@57604
   208
      val old_items = _items
wenzelm@57604
   209
      def was_selected(name: String): Boolean =
wenzelm@57604
   210
        old_items.find(item => item.name == name) match {
wenzelm@57604
   211
          case None => false
wenzelm@57604
   212
          case Some(item) => item.checkbox.selected
wenzelm@57604
   213
        }
wenzelm@57604
   214
wenzelm@57604
   215
      _items =
wenzelm@57604
   216
        Print_Operation.print_operations(PIDE.session).map(
wenzelm@57604
   217
          {
wenzelm@57604
   218
            case (name, description) => new Item(name, description, was_selected(name))
wenzelm@57604
   219
          })
wenzelm@57604
   220
      _items
wenzelm@57604
   221
    }
wenzelm@57604
   222
wenzelm@57604
   223
wenzelm@56864
   224
    /* query */
wenzelm@56864
   225
wenzelm@56909
   226
    private val process_indicator = new Process_Indicator
wenzelm@56909
   227
wenzelm@56864
   228
    val query_operation =
wenzelm@56909
   229
      new Query_Operation(PIDE.editor, view, "print_operation",
wenzelm@56909
   230
        consume_status(process_indicator, _),
wenzelm@56864
   231
        (snapshot, results, body) =>
wenzelm@56864
   232
          pretty_text_area.update(snapshot, results, Pretty.separate(body)))
wenzelm@56864
   233
wenzelm@56864
   234
    private def apply_query()
wenzelm@56864
   235
    {
wenzelm@57604
   236
      query_operation.apply_query(selected_items())
wenzelm@56864
   237
    }
wenzelm@56864
   238
wenzelm@56866
   239
    private val query_label = new Label("Print:")
wenzelm@56882
   240
    def query: JComponent = apply_button.peer
wenzelm@56864
   241
wenzelm@57604
   242
    update_items()
wenzelm@56872
   243
wenzelm@56872
   244
wenzelm@56872
   245
    /* GUI page */
wenzelm@56864
   246
wenzelm@56910
   247
    private val apply_button = new Button("<html><b>Apply</b></html>") {
wenzelm@56865
   248
      tooltip = "Apply to current context"
wenzelm@57000
   249
      listenTo(keys)
wenzelm@57000
   250
      reactions += {
wenzelm@57000
   251
        case ButtonClicked(_) => apply_query()
wenzelm@57000
   252
        case evt @ KeyPressed(_, Key.Enter, 0, _) =>
wenzelm@57000
   253
          evt.peer.consume
wenzelm@57000
   254
          apply_query()
wenzelm@57000
   255
      }
wenzelm@56865
   256
    }
wenzelm@56865
   257
wenzelm@56864
   258
    private val control_panel = new Wrap_Panel(Wrap_Panel.Alignment.Right)()
wenzelm@56864
   259
wenzelm@56864
   260
    def select
wenzelm@56864
   261
    {
wenzelm@56864
   262
      control_panel.contents.clear
wenzelm@57604
   263
      control_panel.contents += query_label
wenzelm@57604
   264
      update_items().foreach(item => control_panel.contents += item.checkbox)
wenzelm@56883
   265
      control_panel.contents ++=
wenzelm@57604
   266
        List(process_indicator.component, apply_button,
wenzelm@57042
   267
          pretty_text_area.search_label, pretty_text_area.search_field, zoom)
wenzelm@56864
   268
    }
wenzelm@56864
   269
wenzelm@56864
   270
    val page =
wenzelm@56879
   271
      new TabbedPane.Page("Print Context", new BorderPanel {
wenzelm@59391
   272
        layout(control_panel) = BorderPanel.Position.North
wenzelm@59391
   273
        layout(Component.wrap(pretty_text_area)) = BorderPanel.Position.Center
wenzelm@56864
   274
      }, "Print information from context")
wenzelm@56864
   275
  }
wenzelm@56864
   276
wenzelm@56864
   277
wenzelm@56757
   278
  /* operations */
wenzelm@56757
   279
wenzelm@56864
   280
  private val operations = List(find_theorems, find_consts, print_operation)
wenzelm@56757
   281
wenzelm@56759
   282
  private val operations_pane = new TabbedPane
wenzelm@56759
   283
  {
wenzelm@56759
   284
    pages ++= operations.map(_.page)
wenzelm@56759
   285
    listenTo(selection)
wenzelm@56759
   286
    reactions += { case SelectionChanged(_) => select_operation() }
wenzelm@56759
   287
  }
wenzelm@56757
   288
wenzelm@56879
   289
  private def get_operation(): Option[Query_Dockable.Operation] =
wenzelm@56759
   290
    try { Some(operations(operations_pane.selection.index)) }
wenzelm@56759
   291
    catch { case _: IndexOutOfBoundsException => None }
wenzelm@56759
   292
wenzelm@56759
   293
  private def select_operation() {
wenzelm@56865
   294
    for (op <- get_operation()) { op.select; op.query.requestFocus }
wenzelm@56759
   295
    operations_pane.revalidate
wenzelm@56757
   296
  }
wenzelm@52865
   297
wenzelm@56759
   298
  override def focusOnDefaultComponent { for (op <- get_operation()) op.query.requestFocus }
wenzelm@56759
   299
wenzelm@56759
   300
  select_operation()
wenzelm@56759
   301
  set_content(operations_pane)
wenzelm@56759
   302
wenzelm@56918
   303
  override def detach_operation =
wenzelm@56918
   304
    get_operation() match {
wenzelm@56918
   305
      case None => None
wenzelm@56918
   306
      case Some(op) => op.pretty_text_area.detach_operation
wenzelm@56918
   307
    }
wenzelm@56906
   308
wenzelm@52865
   309
wenzelm@52865
   310
  /* resize */
wenzelm@52865
   311
wenzelm@56757
   312
  private def handle_resize(): Unit =
wenzelm@57612
   313
    GUI_Thread.require {
wenzelm@56757
   314
      for (op <- operations) {
wenzelm@56757
   315
        op.pretty_text_area.resize(
wenzelm@57044
   316
          Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom.factor / 100))
wenzelm@56757
   317
      }
wenzelm@56757
   318
    }
wenzelm@52846
   319
wenzelm@52865
   320
  private val delay_resize =
wenzelm@57612
   321
    GUI_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
wenzelm@52854
   322
wenzelm@52865
   323
  addComponentListener(new ComponentAdapter {
wenzelm@52865
   324
    override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
wenzelm@60750
   325
    override def componentShown(e: ComponentEvent) { delay_resize.invoke() }
wenzelm@52865
   326
  })
wenzelm@52846
   327
wenzelm@52846
   328
wenzelm@56715
   329
  /* main */
wenzelm@52846
   330
wenzelm@56715
   331
  private val main =
wenzelm@56715
   332
    Session.Consumer[Session.Global_Options](getClass.getName) {
wenzelm@57612
   333
      case _: Session.Global_Options => GUI_Thread.later { handle_resize() }
wenzelm@52846
   334
    }
wenzelm@52846
   335
wenzelm@52846
   336
  override def init()
wenzelm@52846
   337
  {
wenzelm@56715
   338
    PIDE.session.global_options += main
wenzelm@52848
   339
    handle_resize()
wenzelm@56757
   340
    operations.foreach(op => op.query_operation.activate())
wenzelm@52846
   341
  }
wenzelm@52846
   342
wenzelm@52846
   343
  override def exit()
wenzelm@52846
   344
  {
wenzelm@56757
   345
    operations.foreach(op => op.query_operation.deactivate())
wenzelm@56715
   346
    PIDE.session.global_options -= main
wenzelm@52846
   347
    delay_resize.revoke()
wenzelm@52846
   348
  }
wenzelm@56757
   349
}
wenzelm@52846
   350