src/Tools/jEdit/src/find_dockable.scala
author wenzelm
Fri Apr 25 12:51:08 2014 +0200 (2014-04-25)
changeset 56715 52125652e82a
parent 56662 f373fb77e0a4
child 56751 2080e752ed40
permissions -rw-r--r--
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
eliminated old actors;
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@53711
    12
import scala.swing.{Button, Component, TextField, CheckBox, Label, ComboBox}
wenzelm@52846
    13
import scala.swing.event.ButtonClicked
wenzelm@52846
    14
wenzelm@52846
    15
import java.awt.BorderLayout
wenzelm@52886
    16
import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent}
wenzelm@52846
    17
wenzelm@52846
    18
import org.gjt.sp.jedit.View
wenzelm@52846
    19
wenzelm@52846
    20
wenzelm@52846
    21
class Find_Dockable(view: View, position: String) extends Dockable(view, position)
wenzelm@52846
    22
{
wenzelm@52846
    23
  val pretty_text_area = new Pretty_Text_Area(view)
wenzelm@52846
    24
  set_content(pretty_text_area)
wenzelm@52846
    25
wenzelm@52846
    26
wenzelm@52865
    27
  /* query operation */
wenzelm@52865
    28
wenzelm@52935
    29
  private val process_indicator = new Process_Indicator
wenzelm@52935
    30
wenzelm@52935
    31
  private def consume_status(status: Query_Operation.Status.Value)
wenzelm@52935
    32
  {
wenzelm@52935
    33
    status match {
wenzelm@52935
    34
      case Query_Operation.Status.WAITING =>
wenzelm@52935
    35
        process_indicator.update("Waiting for evaluation of context ...", 5)
wenzelm@52935
    36
      case Query_Operation.Status.RUNNING =>
wenzelm@52935
    37
        process_indicator.update("Running find operation ...", 15)
wenzelm@54640
    38
      case Query_Operation.Status.FINISHED =>
wenzelm@52935
    39
        process_indicator.update(null, 0)
wenzelm@52935
    40
    }
wenzelm@52935
    41
  }
wenzelm@52935
    42
wenzelm@52865
    43
  private val find_theorems =
wenzelm@52971
    44
    new Query_Operation(PIDE.editor, view, "find_theorems", consume_status _,
wenzelm@52865
    45
      (snapshot, results, body) =>
wenzelm@52865
    46
        pretty_text_area.update(snapshot, results, Pretty.separate(body)))
wenzelm@52865
    47
wenzelm@52865
    48
wenzelm@52865
    49
  /* resize */
wenzelm@52865
    50
wenzelm@52865
    51
  private var zoom_factor = 100
wenzelm@52865
    52
wenzelm@52846
    53
  private def handle_resize()
wenzelm@52846
    54
  {
wenzelm@56662
    55
    Swing_Thread.require {}
wenzelm@52846
    56
wenzelm@55825
    57
    pretty_text_area.resize(
wenzelm@55825
    58
      Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
wenzelm@52846
    59
  }
wenzelm@52846
    60
wenzelm@52865
    61
  private val delay_resize =
wenzelm@52865
    62
    Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
wenzelm@52854
    63
wenzelm@52865
    64
  addComponentListener(new ComponentAdapter {
wenzelm@52865
    65
    override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
wenzelm@52865
    66
  })
wenzelm@52846
    67
wenzelm@52846
    68
wenzelm@56715
    69
  /* main */
wenzelm@52846
    70
wenzelm@56715
    71
  private val main =
wenzelm@56715
    72
    Session.Consumer[Session.Global_Options](getClass.getName) {
wenzelm@56715
    73
      case _: Session.Global_Options => Swing_Thread.later { handle_resize() }
wenzelm@52846
    74
    }
wenzelm@52846
    75
wenzelm@52846
    76
  override def init()
wenzelm@52846
    77
  {
wenzelm@56715
    78
    PIDE.session.global_options += main
wenzelm@52848
    79
    handle_resize()
wenzelm@52865
    80
    find_theorems.activate()
wenzelm@52846
    81
  }
wenzelm@52846
    82
wenzelm@52846
    83
  override def exit()
wenzelm@52846
    84
  {
wenzelm@52865
    85
    find_theorems.deactivate()
wenzelm@56715
    86
    PIDE.session.global_options -= main
wenzelm@52846
    87
    delay_resize.revoke()
wenzelm@52846
    88
  }
wenzelm@52846
    89
wenzelm@52846
    90
wenzelm@52846
    91
  /* controls */
wenzelm@52846
    92
wenzelm@56621
    93
  private def clicked
wenzelm@56621
    94
  {
wenzelm@56621
    95
    find_theorems.apply_query(List(limit.text, allow_dups.selected.toString, query.getText))
wenzelm@52942
    96
  }
wenzelm@52942
    97
wenzelm@52946
    98
  private val query_label = new Label("Search criteria:") {
wenzelm@54367
    99
    tooltip =
wenzelm@56622
   100
      GUI.tooltip_lines(
wenzelm@56622
   101
        "Search criteria for find operation, e.g.\n\"_ = _\" \"op +\" name: Group -name: monoid")
wenzelm@52946
   102
  }
wenzelm@52886
   103
wenzelm@53784
   104
  private val query = new Completion_Popup.History_Text_Field("isabelle-find-theorems") {
wenzelm@52886
   105
    override def processKeyEvent(evt: KeyEvent)
wenzelm@52886
   106
    {
wenzelm@52886
   107
      if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER) clicked
wenzelm@52886
   108
      super.processKeyEvent(evt)
wenzelm@52886
   109
    }
wenzelm@52846
   110
    { val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) }
wenzelm@52885
   111
    setColumns(40)
wenzelm@52946
   112
    setToolTipText(query_label.tooltip)
wenzelm@55825
   113
    setFont(GUI.imitate_font(Font_Info.main_family(), getFont, 1.2))
wenzelm@52846
   114
  }
wenzelm@52846
   115
wenzelm@52942
   116
  private val limit = new TextField(PIDE.options.int("find_theorems_limit").toString, 5) {
wenzelm@52942
   117
    tooltip = "Limit of displayed results"
wenzelm@52942
   118
    verifier = (s: String) =>
wenzelm@52942
   119
      s match { case Properties.Value.Int(x) => x >= 0 case _ => false }
wenzelm@52942
   120
  }
wenzelm@52942
   121
wenzelm@52942
   122
  private val allow_dups = new CheckBox("Duplicates") {
kleing@52951
   123
    tooltip = "Show all versions of matching theorems"
wenzelm@52942
   124
    selected = false
wenzelm@52942
   125
  }
wenzelm@52846
   126
wenzelm@52880
   127
  private val apply_query = new Button("Apply") {
wenzelm@52846
   128
    tooltip = "Find theorems meeting specified criteria"
wenzelm@52886
   129
    reactions += { case ButtonClicked(_) => clicked }
wenzelm@52846
   130
  }
wenzelm@52846
   131
wenzelm@52846
   132
  private val zoom = new GUI.Zoom_Box(factor => { zoom_factor = factor; handle_resize() }) {
wenzelm@52846
   133
    tooltip = "Zoom factor for output font size"
wenzelm@52846
   134
  }
wenzelm@52846
   135
wenzelm@52846
   136
  private val controls =
wenzelm@53711
   137
    new Wrap_Panel(Wrap_Panel.Alignment.Right)(
wenzelm@56621
   138
      query_label, Component.wrap(query), limit, allow_dups,
wenzelm@52944
   139
      process_indicator.component, apply_query, zoom)
wenzelm@52846
   140
  add(controls.peer, BorderLayout.NORTH)
wenzelm@53787
   141
wenzelm@53787
   142
  override def focusOnDefaultComponent { query.requestFocus }
wenzelm@52846
   143
}