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