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