wenzelm@56879: /*  Title:      Tools/jEdit/src/query_dockable.scala
wenzelm@52846:     Author:     Makarius
wenzelm@52846: 
wenzelm@56879: Dockable window for query operations.
wenzelm@52846: */
wenzelm@52846: 
wenzelm@52846: package isabelle.jedit
wenzelm@52846: 
wenzelm@52846: 
wenzelm@52846: import isabelle._
wenzelm@52846: 
wenzelm@56757: import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent}
wenzelm@56757: import javax.swing.{JComponent, JTextField}
wenzelm@52846: 
wenzelm@56872: import scala.swing.{Button, Component, TextField, CheckBox, Label, ListView,
wenzelm@56757:   ComboBox, TabbedPane, BorderPanel}
wenzelm@56759: import scala.swing.event.{SelectionChanged, ButtonClicked, Key, KeyPressed}
wenzelm@52846: 
wenzelm@52846: import org.gjt.sp.jedit.View
wenzelm@52846: 
wenzelm@52846: 
wenzelm@56879: object Query_Dockable
wenzelm@56757: {
wenzelm@56758:   private abstract class Operation(view: View)
wenzelm@56757:   {
wenzelm@56758:     val pretty_text_area = new Pretty_Text_Area(view)
wenzelm@56757:     def query_operation: Query_Operation[View]
wenzelm@56757:     def query: JComponent
wenzelm@56759:     def select: Unit
wenzelm@56757:     def page: TabbedPane.Page
wenzelm@56757:   }
wenzelm@56757: }
wenzelm@56757: 
wenzelm@56879: class Query_Dockable(view: View, position: String) extends Dockable(view, position)
wenzelm@52846: {
wenzelm@56757:   /* common GUI components */
wenzelm@56757: 
wenzelm@56757:   private var zoom_factor = 100
wenzelm@56757:   private val zoom =
wenzelm@56757:     new GUI.Zoom_Box(factor => if (zoom_factor != factor) { zoom_factor = factor; handle_resize() })
wenzelm@56757:     {
wenzelm@56757:       tooltip = "Zoom factor for output font size"
wenzelm@56757:     }
wenzelm@52846: 
wenzelm@56757:   private def make_query(property: String, tooltip: String, apply_query: () => Unit): JTextField =
wenzelm@56757:     new Completion_Popup.History_Text_Field(property)
wenzelm@56757:     {
wenzelm@56757:       override def processKeyEvent(evt: KeyEvent)
wenzelm@56757:       {
wenzelm@56757:         if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER) apply_query()
wenzelm@56757:         super.processKeyEvent(evt)
wenzelm@56757:       }
wenzelm@56757:       { val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) }
wenzelm@56757:       setColumns(40)
wenzelm@56757:       setToolTipText(tooltip)
wenzelm@56757:       setFont(GUI.imitate_font(Font_Info.main_family(), getFont, 1.2))
wenzelm@56757:     }
wenzelm@52865: 
wenzelm@52935: 
wenzelm@56757:   /* consume status */
wenzelm@56757: 
wenzelm@56757:   def consume_status(process_indicator: Process_Indicator, status: Query_Operation.Status.Value)
wenzelm@52935:   {
wenzelm@52935:     status match {
wenzelm@52935:       case Query_Operation.Status.WAITING =>
wenzelm@52935:         process_indicator.update("Waiting for evaluation of context ...", 5)
wenzelm@52935:       case Query_Operation.Status.RUNNING =>
wenzelm@52935:         process_indicator.update("Running find operation ...", 15)
wenzelm@54640:       case Query_Operation.Status.FINISHED =>
wenzelm@52935:         process_indicator.update(null, 0)
wenzelm@52935:     }
wenzelm@52935:   }
wenzelm@52935: 
wenzelm@56757: 
wenzelm@56757:   /* find theorems */
wenzelm@56757: 
wenzelm@56879:   private val find_theorems = new Query_Dockable.Operation(view)
wenzelm@56757:   {
wenzelm@56757:     /* query */
wenzelm@56757: 
wenzelm@56757:     private val process_indicator = new Process_Indicator
wenzelm@56757: 
wenzelm@56757:     val query_operation =
wenzelm@56757:       new Query_Operation(PIDE.editor, view, "find_theorems",
wenzelm@56757:         consume_status(process_indicator, _),
wenzelm@56757:         (snapshot, results, body) =>
wenzelm@56757:           pretty_text_area.update(snapshot, results, Pretty.separate(body)))
wenzelm@56757: 
wenzelm@56757:     private def apply_query()
wenzelm@56757:     {
wenzelm@56757:       query_operation.apply_query(List(limit.text, allow_dups.selected.toString, query.getText))
wenzelm@56757:     }
wenzelm@56757: 
wenzelm@56883:     private val query_label = new Label("Query:") {
wenzelm@56757:       tooltip =
wenzelm@56757:         GUI.tooltip_lines(
wenzelm@56757:           "Search criteria for find operation, e.g.\n\"_ = _\" \"op +\" name: Group -name: monoid")
wenzelm@56757:     }
wenzelm@56757: 
wenzelm@56757:     val query = make_query("isabelle-find-theorems", query_label.tooltip, apply_query _)
wenzelm@56757: 
wenzelm@56757: 
wenzelm@56758:     /* GUI page */
wenzelm@56757: 
wenzelm@56757:     private val limit = new TextField(PIDE.options.int("find_theorems_limit").toString, 5) {
wenzelm@56757:       tooltip = "Limit of displayed results"
wenzelm@56757:       verifier = (s: String) =>
wenzelm@56757:         s match { case Properties.Value.Int(x) => x >= 0 case _ => false }
wenzelm@56757:       listenTo(keys)
wenzelm@56757:       reactions += { case KeyPressed(_, Key.Enter, 0, _) => apply_query() }
wenzelm@56757:     }
wenzelm@56757: 
wenzelm@56757:     private val allow_dups = new CheckBox("Duplicates") {
wenzelm@56757:       tooltip = "Show all versions of matching theorems"
wenzelm@56757:       selected = false
wenzelm@56757:     }
wenzelm@56757: 
wenzelm@56757:     private val apply_button = new Button("Apply") {
wenzelm@56757:       tooltip = "Find theorems meeting specified criteria"
wenzelm@56757:       reactions += { case ButtonClicked(_) => apply_query() }
wenzelm@56757:     }
wenzelm@56757: 
wenzelm@56759:     private val control_panel =
wenzelm@56759:       new Wrap_Panel(Wrap_Panel.Alignment.Right)(
wenzelm@56759:         query_label, Component.wrap(query), limit, allow_dups,
wenzelm@56886:         process_indicator.component, apply_button, pretty_text_area.detach_button,
wenzelm@56886:         pretty_text_area.search_label, pretty_text_area.search_pattern)
wenzelm@56759: 
wenzelm@56759:     def select { control_panel.contents += zoom }
wenzelm@56757: 
wenzelm@56757:     val page =
wenzelm@56879:       new TabbedPane.Page("Find Theorems", new BorderPanel {
wenzelm@56759:         add(control_panel, BorderPanel.Position.North)
wenzelm@56757:         add(Component.wrap(pretty_text_area), BorderPanel.Position.Center)
wenzelm@56757:       }, apply_button.tooltip)
wenzelm@56757:   }
wenzelm@56757: 
wenzelm@56757: 
wenzelm@56758:   /* find consts */
wenzelm@56758: 
wenzelm@56879:   private val find_consts = new Query_Dockable.Operation(view)
wenzelm@56758:   {
wenzelm@56758:     /* query */
wenzelm@56758: 
wenzelm@56758:     private val process_indicator = new Process_Indicator
wenzelm@56758: 
wenzelm@56758:     val query_operation =
wenzelm@56758:       new Query_Operation(PIDE.editor, view, "find_consts",
wenzelm@56758:         consume_status(process_indicator, _),
wenzelm@56758:         (snapshot, results, body) =>
wenzelm@56758:           pretty_text_area.update(snapshot, results, Pretty.separate(body)))
wenzelm@56758: 
wenzelm@56758:     private def apply_query()
wenzelm@56758:     {
wenzelm@56758:       query_operation.apply_query(List(query.getText))
wenzelm@56758:     }
wenzelm@56758: 
wenzelm@56883:     private val query_label = new Label("Query:") {
wenzelm@56758:       tooltip = GUI.tooltip_lines("Name / type patterns for constants")
wenzelm@56758:     }
wenzelm@56758: 
wenzelm@56758:     val query = make_query("isabelle-find-consts", query_label.tooltip, apply_query _)
wenzelm@56758: 
wenzelm@56758: 
wenzelm@56758:     /* GUI page */
wenzelm@56758: 
wenzelm@56758:     private val apply_button = new Button("Apply") {
wenzelm@56758:       tooltip = "Find constants by name / type patterns"
wenzelm@56758:       reactions += { case ButtonClicked(_) => apply_query() }
wenzelm@56758:     }
wenzelm@56758: 
wenzelm@56759:     private val control_panel =
wenzelm@56759:       new Wrap_Panel(Wrap_Panel.Alignment.Right)(
wenzelm@56886:         query_label, Component.wrap(query), process_indicator.component,
wenzelm@56886:         apply_button, pretty_text_area.detach_button,
wenzelm@56886:         pretty_text_area.search_label, pretty_text_area.search_pattern)
wenzelm@56759: 
wenzelm@56759:     def select { control_panel.contents += zoom }
wenzelm@56758: 
wenzelm@56758:     val page =
wenzelm@56879:       new TabbedPane.Page("Find Constants", new BorderPanel {
wenzelm@56759:         add(control_panel, BorderPanel.Position.North)
wenzelm@56758:         add(Component.wrap(pretty_text_area), BorderPanel.Position.Center)
wenzelm@56758:       }, apply_button.tooltip)
wenzelm@56758:   }
wenzelm@56758: 
wenzelm@56758: 
wenzelm@56864:   /* print operation */
wenzelm@56864: 
wenzelm@56879:   private val print_operation = new Query_Dockable.Operation(view)
wenzelm@56864:   {
wenzelm@56864:     /* query */
wenzelm@56864: 
wenzelm@56864:     val query_operation =
wenzelm@56864:       new Query_Operation(PIDE.editor, view, "print_operation", _ => (),
wenzelm@56864:         (snapshot, results, body) =>
wenzelm@56864:           pretty_text_area.update(snapshot, results, Pretty.separate(body)))
wenzelm@56864: 
wenzelm@56864:     private def apply_query()
wenzelm@56864:     {
wenzelm@56882:       query_operation.apply_query(List(selector.selection.item))
wenzelm@56864:     }
wenzelm@56864: 
wenzelm@56866:     private val query_label = new Label("Print:")
wenzelm@56882:     def query: JComponent = apply_button.peer
wenzelm@56864: 
wenzelm@56864: 
wenzelm@56872:     /* items */
wenzelm@56864: 
wenzelm@56872:     case class Item(name: String, description: String)
wenzelm@56872: 
wenzelm@56872:     class Renderer(old_renderer: ListView.Renderer[String], items: List[Item])
wenzelm@56872:       extends ListView.Renderer[String]
wenzelm@56864:     {
wenzelm@56872:       def componentFor(list: ListView[_],
wenzelm@56872:         selected: Boolean, focused: Boolean, item: String, index: Int) =
wenzelm@56872:       {
wenzelm@56872:         val component = old_renderer.componentFor(list, selected, focused, item, index)
wenzelm@56872:         try { component.tooltip = items(index).description }
wenzelm@56872:         catch { case _: IndexOutOfBoundsException => }
wenzelm@56872:         component
wenzelm@56872:       }
wenzelm@56872:     }
wenzelm@56872: 
wenzelm@56882:     private var selector_item: Option[String] = None
wenzelm@56882:     private var selector = new ComboBox[String](Nil)
wenzelm@56872: 
wenzelm@56872:     private def set_selector()
wenzelm@56872:     {
wenzelm@56872:       val items = Print_Operation.print_operations(PIDE.session).map(p => Item(p._1, p._2))
wenzelm@56872: 
wenzelm@56882:       selector =
wenzelm@56872:         new ComboBox(items.map(_.name)) {
wenzelm@56882:           selector_item.foreach(item => selection.item = item)
wenzelm@56864:           listenTo(selection)
wenzelm@56864:           reactions += {
wenzelm@56864:             case SelectionChanged(_) =>
wenzelm@56882:               selector_item = Some(selection.item)
wenzelm@56864:               apply_query()
wenzelm@56864:           }
wenzelm@56864:         }
wenzelm@56882:       selector.renderer = new Renderer(selector.renderer, items)
wenzelm@56864:     }
wenzelm@56872:     set_selector()
wenzelm@56872: 
wenzelm@56872: 
wenzelm@56872:     /* GUI page */
wenzelm@56864: 
wenzelm@56865:     private val apply_button = new Button("Apply") {
wenzelm@56865:       tooltip = "Apply to current context"
wenzelm@56865:       reactions += { case ButtonClicked(_) => apply_query() }
wenzelm@56865:     }
wenzelm@56865: 
wenzelm@56864:     private val control_panel = new Wrap_Panel(Wrap_Panel.Alignment.Right)()
wenzelm@56864: 
wenzelm@56864:     def select
wenzelm@56864:     {
wenzelm@56872:       set_selector()
wenzelm@56864:       control_panel.contents.clear
wenzelm@56883:       control_panel.contents ++=
wenzelm@56886:         List(query_label, selector, apply_button, pretty_text_area.detach_button,
wenzelm@56886:           pretty_text_area.search_label, pretty_text_area.search_pattern, zoom)
wenzelm@56864:     }
wenzelm@56864: 
wenzelm@56864:     val page =
wenzelm@56879:       new TabbedPane.Page("Print Context", new BorderPanel {
wenzelm@56864:         add(control_panel, BorderPanel.Position.North)
wenzelm@56864:         add(Component.wrap(pretty_text_area), BorderPanel.Position.Center)
wenzelm@56864:       }, "Print information from context")
wenzelm@56864:   }
wenzelm@56864: 
wenzelm@56864: 
wenzelm@56757:   /* operations */
wenzelm@56757: 
wenzelm@56864:   private val operations = List(find_theorems, find_consts, print_operation)
wenzelm@56757: 
wenzelm@56759:   private val operations_pane = new TabbedPane
wenzelm@56759:   {
wenzelm@56759:     pages ++= operations.map(_.page)
wenzelm@56759:     listenTo(selection)
wenzelm@56759:     reactions += { case SelectionChanged(_) => select_operation() }
wenzelm@56759:   }
wenzelm@56757: 
wenzelm@56879:   private def get_operation(): Option[Query_Dockable.Operation] =
wenzelm@56759:     try { Some(operations(operations_pane.selection.index)) }
wenzelm@56759:     catch { case _: IndexOutOfBoundsException => None }
wenzelm@56759: 
wenzelm@56759:   private def select_operation() {
wenzelm@56865:     for (op <- get_operation()) { op.select; op.query.requestFocus }
wenzelm@56759:     operations_pane.revalidate
wenzelm@56757:   }
wenzelm@52865: 
wenzelm@56759:   override def focusOnDefaultComponent { for (op <- get_operation()) op.query.requestFocus }
wenzelm@56759: 
wenzelm@56759:   select_operation()
wenzelm@56759:   set_content(operations_pane)
wenzelm@56759: 
wenzelm@56906:   override val detach_operation = Some(() => get_operation().foreach(_.pretty_text_area.detach))
wenzelm@56906: 
wenzelm@52865: 
wenzelm@52865:   /* resize */
wenzelm@52865: 
wenzelm@56757:   private def handle_resize(): Unit =
wenzelm@56757:     Swing_Thread.require {
wenzelm@56757:       for (op <- operations) {
wenzelm@56757:         op.pretty_text_area.resize(
wenzelm@56757:           Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
wenzelm@56757:       }
wenzelm@56757:     }
wenzelm@52846: 
wenzelm@52865:   private val delay_resize =
wenzelm@52865:     Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
wenzelm@52854: 
wenzelm@52865:   addComponentListener(new ComponentAdapter {
wenzelm@52865:     override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
wenzelm@52865:   })
wenzelm@52846: 
wenzelm@52846: 
wenzelm@56715:   /* main */
wenzelm@52846: 
wenzelm@56715:   private val main =
wenzelm@56715:     Session.Consumer[Session.Global_Options](getClass.getName) {
wenzelm@56715:       case _: Session.Global_Options => Swing_Thread.later { handle_resize() }
wenzelm@52846:     }
wenzelm@52846: 
wenzelm@52846:   override def init()
wenzelm@52846:   {
wenzelm@56715:     PIDE.session.global_options += main
wenzelm@52848:     handle_resize()
wenzelm@56757:     operations.foreach(op => op.query_operation.activate())
wenzelm@52846:   }
wenzelm@52846: 
wenzelm@52846:   override def exit()
wenzelm@52846:   {
wenzelm@56757:     operations.foreach(op => op.query_operation.deactivate())
wenzelm@56715:     PIDE.session.global_options -= main
wenzelm@52846:     delay_resize.revoke()
wenzelm@52846:   }
wenzelm@56757: }
wenzelm@52846: