src/Tools/jEdit/src/find_dockable.scala
author wenzelm
Mon, 05 May 2014 15:17:07 +0200
changeset 56864 0446c7ac2e32
parent 56759 790f7562cd0e
child 56865 168766e28f5e
permissions -rw-r--r--
support print operations as asynchronous query;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
52846
82ac963c68cb dockable window for "find" dialog (GUI only);
wenzelm
parents:
diff changeset
     1
/*  Title:      Tools/jEdit/src/find_dockable.scala
82ac963c68cb dockable window for "find" dialog (GUI only);
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
82ac963c68cb dockable window for "find" dialog (GUI only);
wenzelm
parents:
diff changeset
     3
82ac963c68cb dockable window for "find" dialog (GUI only);
wenzelm
parents:
diff changeset
     4
Dockable window for "find" dialog.
82ac963c68cb dockable window for "find" dialog (GUI only);
wenzelm
parents:
diff changeset
     5
*/
82ac963c68cb dockable window for "find" dialog (GUI only);
wenzelm
parents:
diff changeset
     6
82ac963c68cb dockable window for "find" dialog (GUI only);
wenzelm
parents:
diff changeset
     7
package isabelle.jedit
82ac963c68cb dockable window for "find" dialog (GUI only);
wenzelm
parents:
diff changeset
     8
82ac963c68cb dockable window for "find" dialog (GUI only);
wenzelm
parents:
diff changeset
     9
82ac963c68cb dockable window for "find" dialog (GUI only);
wenzelm
parents:
diff changeset
    10
import isabelle._
82ac963c68cb dockable window for "find" dialog (GUI only);
wenzelm
parents:
diff changeset
    11
56757
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    12
import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent}
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    13
import javax.swing.{JComponent, JTextField}
52846
82ac963c68cb dockable window for "find" dialog (GUI only);
wenzelm
parents:
diff changeset
    14
56757
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    15
import scala.swing.{Button, Component, TextField, CheckBox, Label,
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    16
  ComboBox, TabbedPane, BorderPanel}
56759
790f7562cd0e proper handling of shared zoom component: update layout dynamically;
wenzelm
parents: 56758
diff changeset
    17
import scala.swing.event.{SelectionChanged, ButtonClicked, Key, KeyPressed}
52846
82ac963c68cb dockable window for "find" dialog (GUI only);
wenzelm
parents:
diff changeset
    18
82ac963c68cb dockable window for "find" dialog (GUI only);
wenzelm
parents:
diff changeset
    19
import org.gjt.sp.jedit.View
82ac963c68cb dockable window for "find" dialog (GUI only);
wenzelm
parents:
diff changeset
    20
82ac963c68cb dockable window for "find" dialog (GUI only);
wenzelm
parents:
diff changeset
    21
56757
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    22
object Find_Dockable
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    23
{
56758
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56757
diff changeset
    24
  private abstract class Operation(view: View)
56757
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    25
  {
56758
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56757
diff changeset
    26
    val pretty_text_area = new Pretty_Text_Area(view)
56757
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    27
    def query_operation: Query_Operation[View]
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    28
    def query: JComponent
56759
790f7562cd0e proper handling of shared zoom component: update layout dynamically;
wenzelm
parents: 56758
diff changeset
    29
    def select: Unit
56757
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    30
    def page: TabbedPane.Page
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    31
  }
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    32
}
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    33
52846
82ac963c68cb dockable window for "find" dialog (GUI only);
wenzelm
parents:
diff changeset
    34
class Find_Dockable(view: View, position: String) extends Dockable(view, position)
82ac963c68cb dockable window for "find" dialog (GUI only);
wenzelm
parents:
diff changeset
    35
{
56757
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    36
  /* common GUI components */
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    37
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    38
  private var zoom_factor = 100
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    39
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    40
  private val zoom =
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    41
    new GUI.Zoom_Box(factor => if (zoom_factor != factor) { zoom_factor = factor; handle_resize() })
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    42
    {
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    43
      tooltip = "Zoom factor for output font size"
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    44
    }
52846
82ac963c68cb dockable window for "find" dialog (GUI only);
wenzelm
parents:
diff changeset
    45
82ac963c68cb dockable window for "find" dialog (GUI only);
wenzelm
parents:
diff changeset
    46
56757
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    47
  private def make_query(property: String, tooltip: String, apply_query: () => Unit): JTextField =
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    48
    new Completion_Popup.History_Text_Field(property)
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    49
    {
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    50
      override def processKeyEvent(evt: KeyEvent)
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    51
      {
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    52
        if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER) apply_query()
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    53
        super.processKeyEvent(evt)
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    54
      }
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    55
      { val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) }
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    56
      setColumns(40)
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    57
      setToolTipText(tooltip)
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    58
      setFont(GUI.imitate_font(Font_Info.main_family(), getFont, 1.2))
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    59
    }
52865
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents: 52864
diff changeset
    60
52935
6fc13c31c775 more abstract consume_status operation;
wenzelm
parents: 52886
diff changeset
    61
56757
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    62
  /* consume status */
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    63
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    64
  def consume_status(process_indicator: Process_Indicator, status: Query_Operation.Status.Value)
52935
6fc13c31c775 more abstract consume_status operation;
wenzelm
parents: 52886
diff changeset
    65
  {
6fc13c31c775 more abstract consume_status operation;
wenzelm
parents: 52886
diff changeset
    66
    status match {
6fc13c31c775 more abstract consume_status operation;
wenzelm
parents: 52886
diff changeset
    67
      case Query_Operation.Status.WAITING =>
6fc13c31c775 more abstract consume_status operation;
wenzelm
parents: 52886
diff changeset
    68
        process_indicator.update("Waiting for evaluation of context ...", 5)
6fc13c31c775 more abstract consume_status operation;
wenzelm
parents: 52886
diff changeset
    69
      case Query_Operation.Status.RUNNING =>
6fc13c31c775 more abstract consume_status operation;
wenzelm
parents: 52886
diff changeset
    70
        process_indicator.update("Running find operation ...", 15)
54640
bbd2fa353809 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;
wenzelm
parents: 54368
diff changeset
    71
      case Query_Operation.Status.FINISHED =>
52935
6fc13c31c775 more abstract consume_status operation;
wenzelm
parents: 52886
diff changeset
    72
        process_indicator.update(null, 0)
6fc13c31c775 more abstract consume_status operation;
wenzelm
parents: 52886
diff changeset
    73
    }
6fc13c31c775 more abstract consume_status operation;
wenzelm
parents: 52886
diff changeset
    74
  }
6fc13c31c775 more abstract consume_status operation;
wenzelm
parents: 52886
diff changeset
    75
56757
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    76
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    77
  /* find theorems */
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    78
56758
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56757
diff changeset
    79
  private val find_theorems = new Find_Dockable.Operation(view)
56757
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    80
  {
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    81
    /* query */
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    82
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    83
    private val process_indicator = new Process_Indicator
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    84
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    85
    val query_operation =
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    86
      new Query_Operation(PIDE.editor, view, "find_theorems",
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    87
        consume_status(process_indicator, _),
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    88
        (snapshot, results, body) =>
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    89
          pretty_text_area.update(snapshot, results, Pretty.separate(body)))
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    90
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    91
    private def apply_query()
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    92
    {
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    93
      query_operation.apply_query(List(limit.text, allow_dups.selected.toString, query.getText))
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    94
    }
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    95
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    96
    private val query_label = new Label("Search criteria:") {
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    97
      tooltip =
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    98
        GUI.tooltip_lines(
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
    99
          "Search criteria for find operation, e.g.\n\"_ = _\" \"op +\" name: Group -name: monoid")
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
   100
    }
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
   101
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
   102
    val query = make_query("isabelle-find-theorems", query_label.tooltip, apply_query _)
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
   103
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
   104
56758
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56757
diff changeset
   105
    /* GUI page */
56757
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
   106
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
   107
    private val limit = new TextField(PIDE.options.int("find_theorems_limit").toString, 5) {
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
   108
      tooltip = "Limit of displayed results"
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
   109
      verifier = (s: String) =>
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
   110
        s match { case Properties.Value.Int(x) => x >= 0 case _ => false }
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
   111
      listenTo(keys)
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
   112
      reactions += { case KeyPressed(_, Key.Enter, 0, _) => apply_query() }
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
   113
    }
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
   114
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
   115
    private val allow_dups = new CheckBox("Duplicates") {
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
   116
      tooltip = "Show all versions of matching theorems"
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
   117
      selected = false
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
   118
    }
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
   119
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
   120
    private val apply_button = new Button("Apply") {
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
   121
      tooltip = "Find theorems meeting specified criteria"
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
   122
      reactions += { case ButtonClicked(_) => apply_query() }
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
   123
    }
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
   124
56759
790f7562cd0e proper handling of shared zoom component: update layout dynamically;
wenzelm
parents: 56758
diff changeset
   125
    private val control_panel =
790f7562cd0e proper handling of shared zoom component: update layout dynamically;
wenzelm
parents: 56758
diff changeset
   126
      new Wrap_Panel(Wrap_Panel.Alignment.Right)(
790f7562cd0e proper handling of shared zoom component: update layout dynamically;
wenzelm
parents: 56758
diff changeset
   127
        query_label, Component.wrap(query), limit, allow_dups,
790f7562cd0e proper handling of shared zoom component: update layout dynamically;
wenzelm
parents: 56758
diff changeset
   128
        process_indicator.component, apply_button)
790f7562cd0e proper handling of shared zoom component: update layout dynamically;
wenzelm
parents: 56758
diff changeset
   129
790f7562cd0e proper handling of shared zoom component: update layout dynamically;
wenzelm
parents: 56758
diff changeset
   130
    def select { control_panel.contents += zoom }
56757
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
   131
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
   132
    val page =
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
   133
      new TabbedPane.Page("Theorems", new BorderPanel {
56759
790f7562cd0e proper handling of shared zoom component: update layout dynamically;
wenzelm
parents: 56758
diff changeset
   134
        add(control_panel, BorderPanel.Position.North)
56757
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
   135
        add(Component.wrap(pretty_text_area), BorderPanel.Position.Center)
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
   136
      }, apply_button.tooltip)
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
   137
  }
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
   138
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
   139
56758
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56757
diff changeset
   140
  /* find consts */
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56757
diff changeset
   141
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56757
diff changeset
   142
  private val find_consts = new Find_Dockable.Operation(view)
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56757
diff changeset
   143
  {
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56757
diff changeset
   144
    /* query */
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56757
diff changeset
   145
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56757
diff changeset
   146
    private val process_indicator = new Process_Indicator
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56757
diff changeset
   147
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56757
diff changeset
   148
    val query_operation =
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56757
diff changeset
   149
      new Query_Operation(PIDE.editor, view, "find_consts",
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56757
diff changeset
   150
        consume_status(process_indicator, _),
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56757
diff changeset
   151
        (snapshot, results, body) =>
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56757
diff changeset
   152
          pretty_text_area.update(snapshot, results, Pretty.separate(body)))
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56757
diff changeset
   153
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56757
diff changeset
   154
    private def apply_query()
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56757
diff changeset
   155
    {
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56757
diff changeset
   156
      query_operation.apply_query(List(query.getText))
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56757
diff changeset
   157
    }
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56757
diff changeset
   158
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56757
diff changeset
   159
    private val query_label = new Label("Search criteria:") {
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56757
diff changeset
   160
      tooltip = GUI.tooltip_lines("Name / type patterns for constants")
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56757
diff changeset
   161
    }
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56757
diff changeset
   162
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56757
diff changeset
   163
    val query = make_query("isabelle-find-consts", query_label.tooltip, apply_query _)
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56757
diff changeset
   164
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56757
diff changeset
   165
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56757
diff changeset
   166
    /* GUI page */
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56757
diff changeset
   167
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56757
diff changeset
   168
    private val apply_button = new Button("Apply") {
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56757
diff changeset
   169
      tooltip = "Find constants by name / type patterns"
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56757
diff changeset
   170
      reactions += { case ButtonClicked(_) => apply_query() }
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56757
diff changeset
   171
    }
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56757
diff changeset
   172
56759
790f7562cd0e proper handling of shared zoom component: update layout dynamically;
wenzelm
parents: 56758
diff changeset
   173
    private val control_panel =
790f7562cd0e proper handling of shared zoom component: update layout dynamically;
wenzelm
parents: 56758
diff changeset
   174
      new Wrap_Panel(Wrap_Panel.Alignment.Right)(
790f7562cd0e proper handling of shared zoom component: update layout dynamically;
wenzelm
parents: 56758
diff changeset
   175
        query_label, Component.wrap(query), process_indicator.component, apply_button)
790f7562cd0e proper handling of shared zoom component: update layout dynamically;
wenzelm
parents: 56758
diff changeset
   176
790f7562cd0e proper handling of shared zoom component: update layout dynamically;
wenzelm
parents: 56758
diff changeset
   177
    def select { control_panel.contents += zoom }
56758
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56757
diff changeset
   178
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56757
diff changeset
   179
    val page =
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56757
diff changeset
   180
      new TabbedPane.Page("Constants", new BorderPanel {
56759
790f7562cd0e proper handling of shared zoom component: update layout dynamically;
wenzelm
parents: 56758
diff changeset
   181
        add(control_panel, BorderPanel.Position.North)
56758
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56757
diff changeset
   182
        add(Component.wrap(pretty_text_area), BorderPanel.Position.Center)
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56757
diff changeset
   183
      }, apply_button.tooltip)
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56757
diff changeset
   184
  }
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56757
diff changeset
   185
d203b9c400a2 PIDE support for find_consts;
wenzelm
parents: 56757
diff changeset
   186
56864
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   187
  /* print operation */
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   188
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   189
  private val print_operation = new Find_Dockable.Operation(view)
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   190
  {
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   191
    /* query */
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   192
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   193
    val query_operation =
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   194
      new Query_Operation(PIDE.editor, view, "print_operation", _ => (),
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   195
        (snapshot, results, body) =>
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   196
          pretty_text_area.update(snapshot, results, Pretty.separate(body)))
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   197
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   198
    private var _selector_item = ""
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   199
    private var _selector: ComboBox[String] = null
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   200
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   201
    private def apply_query()
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   202
    {
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   203
      query_operation.apply_query(List(_selector.selection.item))
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   204
    }
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   205
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   206
    def query: JComponent = _selector.peer.asInstanceOf[JComponent]
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   207
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   208
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   209
    /* GUI page */
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   210
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   211
    private def update_selector()
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   212
    {
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   213
      _selector =
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   214
        new ComboBox(Print_Operation.print_operations(PIDE.session).map(_._1)) {
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   215
          selection.item = _selector_item
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   216
          listenTo(selection)
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   217
          reactions += {
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   218
            case SelectionChanged(_) =>
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   219
              _selector_item = selection.item
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   220
              apply_query()
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   221
          }
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   222
        }
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   223
    }
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   224
    update_selector()
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   225
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   226
    private val control_panel = new Wrap_Panel(Wrap_Panel.Alignment.Right)()
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   227
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   228
    def select
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   229
    {
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   230
      update_selector()
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   231
      control_panel.contents.clear
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   232
      control_panel.contents += _selector
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   233
      control_panel.contents += zoom
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   234
      _selector.requestFocus
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   235
    }
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   236
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   237
    val page =
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   238
      new TabbedPane.Page("Print ...", new BorderPanel {
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   239
        add(control_panel, BorderPanel.Position.North)
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   240
        add(Component.wrap(pretty_text_area), BorderPanel.Position.Center)
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   241
      }, "Print information from context")
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   242
  }
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   243
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   244
56757
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
   245
  /* operations */
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
   246
56864
0446c7ac2e32 support print operations as asynchronous query;
wenzelm
parents: 56759
diff changeset
   247
  private val operations = List(find_theorems, find_consts, print_operation)
56757
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
   248
56759
790f7562cd0e proper handling of shared zoom component: update layout dynamically;
wenzelm
parents: 56758
diff changeset
   249
  private val operations_pane = new TabbedPane
790f7562cd0e proper handling of shared zoom component: update layout dynamically;
wenzelm
parents: 56758
diff changeset
   250
  {
790f7562cd0e proper handling of shared zoom component: update layout dynamically;
wenzelm
parents: 56758
diff changeset
   251
    pages ++= operations.map(_.page)
790f7562cd0e proper handling of shared zoom component: update layout dynamically;
wenzelm
parents: 56758
diff changeset
   252
    listenTo(selection)
790f7562cd0e proper handling of shared zoom component: update layout dynamically;
wenzelm
parents: 56758
diff changeset
   253
    reactions += { case SelectionChanged(_) => select_operation() }
790f7562cd0e proper handling of shared zoom component: update layout dynamically;
wenzelm
parents: 56758
diff changeset
   254
  }
56757
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
   255
56759
790f7562cd0e proper handling of shared zoom component: update layout dynamically;
wenzelm
parents: 56758
diff changeset
   256
  private def get_operation(): Option[Find_Dockable.Operation] =
790f7562cd0e proper handling of shared zoom component: update layout dynamically;
wenzelm
parents: 56758
diff changeset
   257
    try { Some(operations(operations_pane.selection.index)) }
790f7562cd0e proper handling of shared zoom component: update layout dynamically;
wenzelm
parents: 56758
diff changeset
   258
    catch { case _: IndexOutOfBoundsException => None }
790f7562cd0e proper handling of shared zoom component: update layout dynamically;
wenzelm
parents: 56758
diff changeset
   259
790f7562cd0e proper handling of shared zoom component: update layout dynamically;
wenzelm
parents: 56758
diff changeset
   260
  private def select_operation() {
790f7562cd0e proper handling of shared zoom component: update layout dynamically;
wenzelm
parents: 56758
diff changeset
   261
    for (op <- get_operation()) op.select
790f7562cd0e proper handling of shared zoom component: update layout dynamically;
wenzelm
parents: 56758
diff changeset
   262
    operations_pane.revalidate
56757
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
   263
  }
52865
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents: 52864
diff changeset
   264
56759
790f7562cd0e proper handling of shared zoom component: update layout dynamically;
wenzelm
parents: 56758
diff changeset
   265
  override def focusOnDefaultComponent { for (op <- get_operation()) op.query.requestFocus }
790f7562cd0e proper handling of shared zoom component: update layout dynamically;
wenzelm
parents: 56758
diff changeset
   266
790f7562cd0e proper handling of shared zoom component: update layout dynamically;
wenzelm
parents: 56758
diff changeset
   267
  select_operation()
790f7562cd0e proper handling of shared zoom component: update layout dynamically;
wenzelm
parents: 56758
diff changeset
   268
  set_content(operations_pane)
790f7562cd0e proper handling of shared zoom component: update layout dynamically;
wenzelm
parents: 56758
diff changeset
   269
52865
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents: 52864
diff changeset
   270
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents: 52864
diff changeset
   271
  /* resize */
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents: 52864
diff changeset
   272
56757
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
   273
  private def handle_resize(): Unit =
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
   274
    Swing_Thread.require {
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
   275
      for (op <- operations) {
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
   276
        op.pretty_text_area.resize(
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
   277
          Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
   278
      }
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
   279
    }
52846
82ac963c68cb dockable window for "find" dialog (GUI only);
wenzelm
parents:
diff changeset
   280
52865
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents: 52864
diff changeset
   281
  private val delay_resize =
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents: 52864
diff changeset
   282
    Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
52854
92932931bd82 more general Output.result: allow to update arbitrary properties;
wenzelm
parents: 52851
diff changeset
   283
52865
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents: 52864
diff changeset
   284
  addComponentListener(new ComponentAdapter {
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents: 52864
diff changeset
   285
    override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
02a7e7180ee5 slightly more general support for one-shot query operations via asynchronous print functions and temporary document overlay;
wenzelm
parents: 52864
diff changeset
   286
  })
52846
82ac963c68cb dockable window for "find" dialog (GUI only);
wenzelm
parents:
diff changeset
   287
82ac963c68cb dockable window for "find" dialog (GUI only);
wenzelm
parents:
diff changeset
   288
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
   289
  /* main */
52846
82ac963c68cb dockable window for "find" dialog (GUI only);
wenzelm
parents:
diff changeset
   290
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
   291
  private val main =
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
   292
    Session.Consumer[Session.Global_Options](getClass.getName) {
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
   293
      case _: Session.Global_Options => Swing_Thread.later { handle_resize() }
52846
82ac963c68cb dockable window for "find" dialog (GUI only);
wenzelm
parents:
diff changeset
   294
    }
82ac963c68cb dockable window for "find" dialog (GUI only);
wenzelm
parents:
diff changeset
   295
82ac963c68cb dockable window for "find" dialog (GUI only);
wenzelm
parents:
diff changeset
   296
  override def init()
82ac963c68cb dockable window for "find" dialog (GUI only);
wenzelm
parents:
diff changeset
   297
  {
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
   298
    PIDE.session.global_options += main
52848
9489ca1d55dd some tracking of command location;
wenzelm
parents: 52846
diff changeset
   299
    handle_resize()
56757
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
   300
    operations.foreach(op => op.query_operation.activate())
52846
82ac963c68cb dockable window for "find" dialog (GUI only);
wenzelm
parents:
diff changeset
   301
  }
82ac963c68cb dockable window for "find" dialog (GUI only);
wenzelm
parents:
diff changeset
   302
82ac963c68cb dockable window for "find" dialog (GUI only);
wenzelm
parents:
diff changeset
   303
  override def exit()
82ac963c68cb dockable window for "find" dialog (GUI only);
wenzelm
parents:
diff changeset
   304
  {
56757
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
   305
    operations.foreach(op => op.query_operation.deactivate())
56715
52125652e82a clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents: 56662
diff changeset
   306
    PIDE.session.global_options -= main
52846
82ac963c68cb dockable window for "find" dialog (GUI only);
wenzelm
parents:
diff changeset
   307
    delay_resize.revoke()
82ac963c68cb dockable window for "find" dialog (GUI only);
wenzelm
parents:
diff changeset
   308
  }
56757
d6fdf08282f3 some rearrangements to support multiple find operations;
wenzelm
parents: 56751
diff changeset
   309
}
52846
82ac963c68cb dockable window for "find" dialog (GUI only);
wenzelm
parents:
diff changeset
   310