src/Tools/jEdit/src/find_dockable.scala
author wenzelm
Thu Nov 21 21:55:29 2013 +0100 (2013-11-21)
changeset 54640 bbd2fa353809
parent 54368 36dc6aa4fe87
child 55618 995162143ef4
permissions -rw-r--r--
back to Status.FINISHED and immediate remove_overlay (reverting 6e69f9ca8f1c), which is important to avoid restart of print function after edits + re-assignment of located command;
resolve sendback wrt. static command id, to allow active area even after exec_id is removed (cf. prune_delay);
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@52846
    12
import scala.actors.Actor._
wenzelm@52846
    13
wenzelm@53711
    14
import scala.swing.{Button, Component, TextField, CheckBox, Label, ComboBox}
wenzelm@52846
    15
import scala.swing.event.ButtonClicked
wenzelm@52846
    16
wenzelm@52846
    17
import java.awt.BorderLayout
wenzelm@52886
    18
import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent}
wenzelm@52846
    19
wenzelm@52846
    20
import org.gjt.sp.jedit.View
wenzelm@52846
    21
wenzelm@52846
    22
wenzelm@52846
    23
class Find_Dockable(view: View, position: String) extends Dockable(view, position)
wenzelm@52846
    24
{
wenzelm@52846
    25
  val pretty_text_area = new Pretty_Text_Area(view)
wenzelm@52846
    26
  set_content(pretty_text_area)
wenzelm@52846
    27
wenzelm@52846
    28
wenzelm@52865
    29
  /* query operation */
wenzelm@52865
    30
wenzelm@52935
    31
  private val process_indicator = new Process_Indicator
wenzelm@52935
    32
wenzelm@52935
    33
  private def consume_status(status: Query_Operation.Status.Value)
wenzelm@52935
    34
  {
wenzelm@52935
    35
    status match {
wenzelm@52935
    36
      case Query_Operation.Status.WAITING =>
wenzelm@52935
    37
        process_indicator.update("Waiting for evaluation of context ...", 5)
wenzelm@52935
    38
      case Query_Operation.Status.RUNNING =>
wenzelm@52935
    39
        process_indicator.update("Running find operation ...", 15)
wenzelm@54640
    40
      case Query_Operation.Status.FINISHED =>
wenzelm@52935
    41
        process_indicator.update(null, 0)
wenzelm@52935
    42
    }
wenzelm@52935
    43
  }
wenzelm@52935
    44
wenzelm@52865
    45
  private val find_theorems =
wenzelm@52971
    46
    new Query_Operation(PIDE.editor, view, "find_theorems", consume_status _,
wenzelm@52865
    47
      (snapshot, results, body) =>
wenzelm@52865
    48
        pretty_text_area.update(snapshot, results, Pretty.separate(body)))
wenzelm@52865
    49
wenzelm@52865
    50
wenzelm@52865
    51
  /* resize */
wenzelm@52865
    52
wenzelm@52865
    53
  private var zoom_factor = 100
wenzelm@52865
    54
wenzelm@52846
    55
  private def handle_resize()
wenzelm@52846
    56
  {
wenzelm@52846
    57
    Swing_Thread.require()
wenzelm@52846
    58
wenzelm@52846
    59
    pretty_text_area.resize(Rendering.font_family(),
wenzelm@52846
    60
      (Rendering.font_size("jedit_font_scale") * zoom_factor / 100).round)
wenzelm@52846
    61
  }
wenzelm@52846
    62
wenzelm@52865
    63
  private val delay_resize =
wenzelm@52865
    64
    Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
wenzelm@52854
    65
wenzelm@52865
    66
  addComponentListener(new ComponentAdapter {
wenzelm@52865
    67
    override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
wenzelm@52865
    68
  })
wenzelm@52846
    69
wenzelm@52846
    70
wenzelm@52846
    71
  /* main actor */
wenzelm@52846
    72
wenzelm@52846
    73
  private val main_actor = actor {
wenzelm@52846
    74
    loop {
wenzelm@52846
    75
      react {
wenzelm@52846
    76
        case _: Session.Global_Options =>
wenzelm@52846
    77
          Swing_Thread.later { handle_resize() }
wenzelm@53177
    78
wenzelm@52846
    79
        case bad =>
wenzelm@52846
    80
          java.lang.System.err.println("Find_Dockable: ignoring bad message " + bad)
wenzelm@52846
    81
      }
wenzelm@52846
    82
    }
wenzelm@52846
    83
  }
wenzelm@52846
    84
wenzelm@52846
    85
  override def init()
wenzelm@52846
    86
  {
wenzelm@52846
    87
    PIDE.session.global_options += main_actor
wenzelm@52848
    88
    handle_resize()
wenzelm@52865
    89
    find_theorems.activate()
wenzelm@52846
    90
  }
wenzelm@52846
    91
wenzelm@52846
    92
  override def exit()
wenzelm@52846
    93
  {
wenzelm@52865
    94
    find_theorems.deactivate()
wenzelm@52846
    95
    PIDE.session.global_options -= main_actor
wenzelm@52846
    96
    delay_resize.revoke()
wenzelm@52846
    97
  }
wenzelm@52846
    98
wenzelm@52846
    99
wenzelm@52846
   100
  /* controls */
wenzelm@52846
   101
wenzelm@52942
   102
  private def clicked {
wenzelm@52943
   103
    find_theorems.apply_query(
wenzelm@52943
   104
      List(limit.text, allow_dups.selected.toString, context.selection.item.name, query.getText))
wenzelm@52942
   105
  }
wenzelm@52942
   106
wenzelm@52946
   107
  private val query_label = new Label("Search criteria:") {
wenzelm@54367
   108
    tooltip =
wenzelm@54367
   109
      GUI.tooltip_lines(List(
wenzelm@54367
   110
        "Search criteria for find operation, e.g.",
wenzelm@54367
   111
        "",
wenzelm@54367
   112
        "  \"_ = _\" \"op +\" name: Group -name: monoid"))
wenzelm@52946
   113
  }
wenzelm@52886
   114
wenzelm@53784
   115
  private val query = new Completion_Popup.History_Text_Field("isabelle-find-theorems") {
wenzelm@52886
   116
    override def processKeyEvent(evt: KeyEvent)
wenzelm@52886
   117
    {
wenzelm@52886
   118
      if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER) clicked
wenzelm@52886
   119
      super.processKeyEvent(evt)
wenzelm@52886
   120
    }
wenzelm@52846
   121
    { val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) }
wenzelm@52885
   122
    setColumns(40)
wenzelm@52946
   123
    setToolTipText(query_label.tooltip)
wenzelm@54368
   124
    setFont(GUI.imitate_font(Rendering.font_family(), getFont, 1.2))
wenzelm@52846
   125
  }
wenzelm@52846
   126
wenzelm@52943
   127
  private case class Context_Entry(val name: String, val description: String)
wenzelm@52943
   128
  {
wenzelm@52943
   129
    override def toString = description
wenzelm@52943
   130
  }
wenzelm@52943
   131
wenzelm@52943
   132
  private val context_entries =
wenzelm@52946
   133
    new Context_Entry("", "current context") ::
wenzelm@52943
   134
      PIDE.thy_load.loaded_theories.toList.sorted.map(name => Context_Entry(name, name))
wenzelm@52943
   135
wenzelm@52943
   136
  private val context = new ComboBox[Context_Entry](context_entries) {
wenzelm@52943
   137
    tooltip = "Search in pre-loaded theory (default: context of current command)"
wenzelm@52943
   138
  }
wenzelm@52943
   139
wenzelm@52942
   140
  private val limit = new TextField(PIDE.options.int("find_theorems_limit").toString, 5) {
wenzelm@52942
   141
    tooltip = "Limit of displayed results"
wenzelm@52942
   142
    verifier = (s: String) =>
wenzelm@52942
   143
      s match { case Properties.Value.Int(x) => x >= 0 case _ => false }
wenzelm@52942
   144
  }
wenzelm@52942
   145
wenzelm@52942
   146
  private val allow_dups = new CheckBox("Duplicates") {
kleing@52951
   147
    tooltip = "Show all versions of matching theorems"
wenzelm@52942
   148
    selected = false
wenzelm@52942
   149
  }
wenzelm@52846
   150
wenzelm@52880
   151
  private val apply_query = new Button("Apply") {
wenzelm@52846
   152
    tooltip = "Find theorems meeting specified criteria"
wenzelm@52886
   153
    reactions += { case ButtonClicked(_) => clicked }
wenzelm@52846
   154
  }
wenzelm@52846
   155
wenzelm@52846
   156
  private val zoom = new GUI.Zoom_Box(factor => { zoom_factor = factor; handle_resize() }) {
wenzelm@52846
   157
    tooltip = "Zoom factor for output font size"
wenzelm@52846
   158
  }
wenzelm@52846
   159
wenzelm@52846
   160
  private val controls =
wenzelm@53711
   161
    new Wrap_Panel(Wrap_Panel.Alignment.Right)(
wenzelm@52943
   162
      query_label, Component.wrap(query), context, limit, allow_dups,
wenzelm@52944
   163
      process_indicator.component, apply_query, zoom)
wenzelm@52846
   164
  add(controls.peer, BorderLayout.NORTH)
wenzelm@53787
   165
wenzelm@53787
   166
  override def focusOnDefaultComponent { query.requestFocus }
wenzelm@52846
   167
}