src/Tools/jEdit/src/find_dockable.scala
author wenzelm
Sat Apr 26 21:49:31 2014 +0200 (2014-04-26)
changeset 56758 d203b9c400a2
parent 56757 d6fdf08282f3
child 56759 790f7562cd0e
permissions -rw-r--r--
PIDE support for find_consts;
wenzelm@52846
     1
/*  Title:      Tools/jEdit/src/find_dockable.scala
wenzelm@52846
     2
    Author:     Makarius
wenzelm@52846
     3
wenzelm@52846
     4
Dockable window for "find" dialog.
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@56757
    15
import scala.swing.{Button, Component, TextField, CheckBox, Label,
wenzelm@56757
    16
  ComboBox, TabbedPane, BorderPanel}
wenzelm@56757
    17
import scala.swing.event.{ButtonClicked, Key, KeyPressed}
wenzelm@52846
    18
wenzelm@52846
    19
import org.gjt.sp.jedit.View
wenzelm@52846
    20
wenzelm@52846
    21
wenzelm@56757
    22
object Find_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@56757
    29
    def page: TabbedPane.Page
wenzelm@56757
    30
  }
wenzelm@56757
    31
}
wenzelm@56757
    32
wenzelm@52846
    33
class Find_Dockable(view: View, position: String) extends Dockable(view, position)
wenzelm@52846
    34
{
wenzelm@56757
    35
  /* common GUI components */
wenzelm@56757
    36
wenzelm@56757
    37
  private var zoom_factor = 100
wenzelm@56757
    38
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@52846
    45
wenzelm@56757
    46
  private def make_query(property: String, tooltip: String, apply_query: () => Unit): JTextField =
wenzelm@56757
    47
    new Completion_Popup.History_Text_Field(property)
wenzelm@56757
    48
    {
wenzelm@56757
    49
      override def processKeyEvent(evt: KeyEvent)
wenzelm@56757
    50
      {
wenzelm@56757
    51
        if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER) apply_query()
wenzelm@56757
    52
        super.processKeyEvent(evt)
wenzelm@56757
    53
      }
wenzelm@56757
    54
      { val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) }
wenzelm@56757
    55
      setColumns(40)
wenzelm@56757
    56
      setToolTipText(tooltip)
wenzelm@56757
    57
      setFont(GUI.imitate_font(Font_Info.main_family(), getFont, 1.2))
wenzelm@56757
    58
    }
wenzelm@52865
    59
wenzelm@52935
    60
wenzelm@56757
    61
  /* consume status */
wenzelm@56757
    62
wenzelm@56757
    63
  def consume_status(process_indicator: Process_Indicator, status: Query_Operation.Status.Value)
wenzelm@52935
    64
  {
wenzelm@52935
    65
    status match {
wenzelm@52935
    66
      case Query_Operation.Status.WAITING =>
wenzelm@52935
    67
        process_indicator.update("Waiting for evaluation of context ...", 5)
wenzelm@52935
    68
      case Query_Operation.Status.RUNNING =>
wenzelm@52935
    69
        process_indicator.update("Running find operation ...", 15)
wenzelm@54640
    70
      case Query_Operation.Status.FINISHED =>
wenzelm@52935
    71
        process_indicator.update(null, 0)
wenzelm@52935
    72
    }
wenzelm@52935
    73
  }
wenzelm@52935
    74
wenzelm@56757
    75
wenzelm@56757
    76
  /* find theorems */
wenzelm@56757
    77
wenzelm@56758
    78
  private val find_theorems = new Find_Dockable.Operation(view)
wenzelm@56757
    79
  {
wenzelm@56757
    80
    /* query */
wenzelm@56757
    81
wenzelm@56757
    82
    private val process_indicator = new Process_Indicator
wenzelm@56757
    83
wenzelm@56757
    84
    val query_operation =
wenzelm@56757
    85
      new Query_Operation(PIDE.editor, view, "find_theorems",
wenzelm@56757
    86
        consume_status(process_indicator, _),
wenzelm@56757
    87
        (snapshot, results, body) =>
wenzelm@56757
    88
          pretty_text_area.update(snapshot, results, Pretty.separate(body)))
wenzelm@56757
    89
wenzelm@56757
    90
    private def apply_query()
wenzelm@56757
    91
    {
wenzelm@56757
    92
      query_operation.apply_query(List(limit.text, allow_dups.selected.toString, query.getText))
wenzelm@56757
    93
    }
wenzelm@56757
    94
wenzelm@56757
    95
    private val query_label = new Label("Search criteria:") {
wenzelm@56757
    96
      tooltip =
wenzelm@56757
    97
        GUI.tooltip_lines(
wenzelm@56757
    98
          "Search criteria for find operation, e.g.\n\"_ = _\" \"op +\" name: Group -name: monoid")
wenzelm@56757
    99
    }
wenzelm@56757
   100
wenzelm@56757
   101
    val query = make_query("isabelle-find-theorems", query_label.tooltip, apply_query _)
wenzelm@56757
   102
wenzelm@56757
   103
wenzelm@56758
   104
    /* GUI page */
wenzelm@56757
   105
wenzelm@56757
   106
    private val limit = new TextField(PIDE.options.int("find_theorems_limit").toString, 5) {
wenzelm@56757
   107
      tooltip = "Limit of displayed results"
wenzelm@56757
   108
      verifier = (s: String) =>
wenzelm@56757
   109
        s match { case Properties.Value.Int(x) => x >= 0 case _ => false }
wenzelm@56757
   110
      listenTo(keys)
wenzelm@56757
   111
      reactions += { case KeyPressed(_, Key.Enter, 0, _) => apply_query() }
wenzelm@56757
   112
    }
wenzelm@56757
   113
wenzelm@56757
   114
    private val allow_dups = new CheckBox("Duplicates") {
wenzelm@56757
   115
      tooltip = "Show all versions of matching theorems"
wenzelm@56757
   116
      selected = false
wenzelm@56757
   117
    }
wenzelm@56757
   118
wenzelm@56757
   119
    private val apply_button = new Button("Apply") {
wenzelm@56757
   120
      tooltip = "Find theorems meeting specified criteria"
wenzelm@56757
   121
      reactions += { case ButtonClicked(_) => apply_query() }
wenzelm@56757
   122
    }
wenzelm@56757
   123
wenzelm@56757
   124
    private val controls: List[Component] =
wenzelm@56757
   125
      List(query_label, Component.wrap(query), limit, allow_dups,
wenzelm@56757
   126
        process_indicator.component, apply_button, zoom)
wenzelm@56757
   127
wenzelm@56757
   128
    val page =
wenzelm@56757
   129
      new TabbedPane.Page("Theorems", new BorderPanel {
wenzelm@56757
   130
        add(new Wrap_Panel(Wrap_Panel.Alignment.Right)(controls:_*), BorderPanel.Position.North)
wenzelm@56757
   131
        add(Component.wrap(pretty_text_area), BorderPanel.Position.Center)
wenzelm@56757
   132
      }, apply_button.tooltip)
wenzelm@56757
   133
  }
wenzelm@56757
   134
wenzelm@56757
   135
wenzelm@56758
   136
  /* find consts */
wenzelm@56758
   137
wenzelm@56758
   138
  private val find_consts = new Find_Dockable.Operation(view)
wenzelm@56758
   139
  {
wenzelm@56758
   140
    /* query */
wenzelm@56758
   141
wenzelm@56758
   142
    private val process_indicator = new Process_Indicator
wenzelm@56758
   143
wenzelm@56758
   144
    val query_operation =
wenzelm@56758
   145
      new Query_Operation(PIDE.editor, view, "find_consts",
wenzelm@56758
   146
        consume_status(process_indicator, _),
wenzelm@56758
   147
        (snapshot, results, body) =>
wenzelm@56758
   148
          pretty_text_area.update(snapshot, results, Pretty.separate(body)))
wenzelm@56758
   149
wenzelm@56758
   150
    private def apply_query()
wenzelm@56758
   151
    {
wenzelm@56758
   152
      query_operation.apply_query(List(query.getText))
wenzelm@56758
   153
    }
wenzelm@56758
   154
wenzelm@56758
   155
    private val query_label = new Label("Search criteria:") {
wenzelm@56758
   156
      tooltip = GUI.tooltip_lines("Name / type patterns for constants")
wenzelm@56758
   157
    }
wenzelm@56758
   158
wenzelm@56758
   159
    val query = make_query("isabelle-find-consts", query_label.tooltip, apply_query _)
wenzelm@56758
   160
wenzelm@56758
   161
wenzelm@56758
   162
    /* GUI page */
wenzelm@56758
   163
wenzelm@56758
   164
    private val apply_button = new Button("Apply") {
wenzelm@56758
   165
      tooltip = "Find constants by name / type patterns"
wenzelm@56758
   166
      reactions += { case ButtonClicked(_) => apply_query() }
wenzelm@56758
   167
    }
wenzelm@56758
   168
wenzelm@56758
   169
    private val controls: List[Component] =
wenzelm@56758
   170
      List(query_label, Component.wrap(query), process_indicator.component, apply_button, zoom)
wenzelm@56758
   171
wenzelm@56758
   172
    val page =
wenzelm@56758
   173
      new TabbedPane.Page("Constants", new BorderPanel {
wenzelm@56758
   174
        add(new Wrap_Panel(Wrap_Panel.Alignment.Right)(controls:_*), BorderPanel.Position.North)
wenzelm@56758
   175
        add(Component.wrap(pretty_text_area), BorderPanel.Position.Center)
wenzelm@56758
   176
      }, apply_button.tooltip)
wenzelm@56758
   177
  }
wenzelm@56758
   178
wenzelm@56758
   179
wenzelm@56757
   180
  /* operations */
wenzelm@56757
   181
wenzelm@56758
   182
  private val operations = List(find_theorems, find_consts)
wenzelm@56757
   183
wenzelm@56757
   184
  private val tabs = new TabbedPane { for (op <- operations) pages += op.page }
wenzelm@56757
   185
  set_content(tabs)
wenzelm@56757
   186
wenzelm@56757
   187
  override def focusOnDefaultComponent {
wenzelm@56757
   188
    try { operations(tabs.selection.index).query.requestFocus }
wenzelm@56757
   189
    catch { case _: IndexOutOfBoundsException => }
wenzelm@56757
   190
  }
wenzelm@52865
   191
wenzelm@52865
   192
wenzelm@52865
   193
  /* resize */
wenzelm@52865
   194
wenzelm@56757
   195
  private def handle_resize(): Unit =
wenzelm@56757
   196
    Swing_Thread.require {
wenzelm@56757
   197
      for (op <- operations) {
wenzelm@56757
   198
        op.pretty_text_area.resize(
wenzelm@56757
   199
          Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
wenzelm@56757
   200
      }
wenzelm@56757
   201
    }
wenzelm@52846
   202
wenzelm@52865
   203
  private val delay_resize =
wenzelm@52865
   204
    Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
wenzelm@52854
   205
wenzelm@52865
   206
  addComponentListener(new ComponentAdapter {
wenzelm@52865
   207
    override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
wenzelm@52865
   208
  })
wenzelm@52846
   209
wenzelm@52846
   210
wenzelm@56715
   211
  /* main */
wenzelm@52846
   212
wenzelm@56715
   213
  private val main =
wenzelm@56715
   214
    Session.Consumer[Session.Global_Options](getClass.getName) {
wenzelm@56715
   215
      case _: Session.Global_Options => Swing_Thread.later { handle_resize() }
wenzelm@52846
   216
    }
wenzelm@52846
   217
wenzelm@52846
   218
  override def init()
wenzelm@52846
   219
  {
wenzelm@56715
   220
    PIDE.session.global_options += main
wenzelm@52848
   221
    handle_resize()
wenzelm@56757
   222
    operations.foreach(op => op.query_operation.activate())
wenzelm@52846
   223
  }
wenzelm@52846
   224
wenzelm@52846
   225
  override def exit()
wenzelm@52846
   226
  {
wenzelm@56757
   227
    operations.foreach(op => op.query_operation.deactivate())
wenzelm@56715
   228
    PIDE.session.global_options -= main
wenzelm@52846
   229
    delay_resize.revoke()
wenzelm@52846
   230
  }
wenzelm@56757
   231
}
wenzelm@52846
   232