src/Tools/jEdit/src/find_dockable.scala
author wenzelm
Fri Apr 25 12:51:08 2014 +0200 (2014-04-25)
changeset 56715 52125652e82a
parent 56662 f373fb77e0a4
child 56751 2080e752ed40
permissions -rw-r--r--
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
eliminated old actors;
     1 /*  Title:      Tools/jEdit/src/find_dockable.scala
     2     Author:     Makarius
     3 
     4 Dockable window for "find" dialog.
     5 */
     6 
     7 package isabelle.jedit
     8 
     9 
    10 import isabelle._
    11 
    12 import scala.swing.{Button, Component, TextField, CheckBox, Label, ComboBox}
    13 import scala.swing.event.ButtonClicked
    14 
    15 import java.awt.BorderLayout
    16 import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent}
    17 
    18 import org.gjt.sp.jedit.View
    19 
    20 
    21 class Find_Dockable(view: View, position: String) extends Dockable(view, position)
    22 {
    23   val pretty_text_area = new Pretty_Text_Area(view)
    24   set_content(pretty_text_area)
    25 
    26 
    27   /* query operation */
    28 
    29   private val process_indicator = new Process_Indicator
    30 
    31   private def consume_status(status: Query_Operation.Status.Value)
    32   {
    33     status match {
    34       case Query_Operation.Status.WAITING =>
    35         process_indicator.update("Waiting for evaluation of context ...", 5)
    36       case Query_Operation.Status.RUNNING =>
    37         process_indicator.update("Running find operation ...", 15)
    38       case Query_Operation.Status.FINISHED =>
    39         process_indicator.update(null, 0)
    40     }
    41   }
    42 
    43   private val find_theorems =
    44     new Query_Operation(PIDE.editor, view, "find_theorems", consume_status _,
    45       (snapshot, results, body) =>
    46         pretty_text_area.update(snapshot, results, Pretty.separate(body)))
    47 
    48 
    49   /* resize */
    50 
    51   private var zoom_factor = 100
    52 
    53   private def handle_resize()
    54   {
    55     Swing_Thread.require {}
    56 
    57     pretty_text_area.resize(
    58       Font_Info.main(PIDE.options.real("jedit_font_scale") * zoom_factor / 100))
    59   }
    60 
    61   private val delay_resize =
    62     Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
    63 
    64   addComponentListener(new ComponentAdapter {
    65     override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
    66   })
    67 
    68 
    69   /* main */
    70 
    71   private val main =
    72     Session.Consumer[Session.Global_Options](getClass.getName) {
    73       case _: Session.Global_Options => Swing_Thread.later { handle_resize() }
    74     }
    75 
    76   override def init()
    77   {
    78     PIDE.session.global_options += main
    79     handle_resize()
    80     find_theorems.activate()
    81   }
    82 
    83   override def exit()
    84   {
    85     find_theorems.deactivate()
    86     PIDE.session.global_options -= main
    87     delay_resize.revoke()
    88   }
    89 
    90 
    91   /* controls */
    92 
    93   private def clicked
    94   {
    95     find_theorems.apply_query(List(limit.text, allow_dups.selected.toString, query.getText))
    96   }
    97 
    98   private val query_label = new Label("Search criteria:") {
    99     tooltip =
   100       GUI.tooltip_lines(
   101         "Search criteria for find operation, e.g.\n\"_ = _\" \"op +\" name: Group -name: monoid")
   102   }
   103 
   104   private val query = new Completion_Popup.History_Text_Field("isabelle-find-theorems") {
   105     override def processKeyEvent(evt: KeyEvent)
   106     {
   107       if (evt.getID == KeyEvent.KEY_PRESSED && evt.getKeyCode == KeyEvent.VK_ENTER) clicked
   108       super.processKeyEvent(evt)
   109     }
   110     { val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) }
   111     setColumns(40)
   112     setToolTipText(query_label.tooltip)
   113     setFont(GUI.imitate_font(Font_Info.main_family(), getFont, 1.2))
   114   }
   115 
   116   private val limit = new TextField(PIDE.options.int("find_theorems_limit").toString, 5) {
   117     tooltip = "Limit of displayed results"
   118     verifier = (s: String) =>
   119       s match { case Properties.Value.Int(x) => x >= 0 case _ => false }
   120   }
   121 
   122   private val allow_dups = new CheckBox("Duplicates") {
   123     tooltip = "Show all versions of matching theorems"
   124     selected = false
   125   }
   126 
   127   private val apply_query = new Button("Apply") {
   128     tooltip = "Find theorems meeting specified criteria"
   129     reactions += { case ButtonClicked(_) => clicked }
   130   }
   131 
   132   private val zoom = new GUI.Zoom_Box(factor => { zoom_factor = factor; handle_resize() }) {
   133     tooltip = "Zoom factor for output font size"
   134   }
   135 
   136   private val controls =
   137     new Wrap_Panel(Wrap_Panel.Alignment.Right)(
   138       query_label, Component.wrap(query), limit, allow_dups,
   139       process_indicator.component, apply_query, zoom)
   140   add(controls.peer, BorderLayout.NORTH)
   141 
   142   override def focusOnDefaultComponent { query.requestFocus }
   143 }