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