src/Tools/jEdit/src/find_dockable.scala
author wenzelm
Fri Aug 02 16:02:06 2013 +0200 (2013-08-02)
changeset 52851 e71b5160f242
parent 52848 9489ca1d55dd
child 52854 92932931bd82
permissions -rw-r--r--
minimal print function "find_theorems", which merely echos its arguments;
     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.actors.Actor._
    13 
    14 import scala.swing.{FlowPanel, Button, Component}
    15 import scala.swing.event.ButtonClicked
    16 
    17 import java.awt.BorderLayout
    18 import java.awt.event.{ComponentEvent, ComponentAdapter}
    19 
    20 import org.gjt.sp.jedit.View
    21 import org.gjt.sp.jedit.gui.HistoryTextArea
    22 
    23 
    24 class Find_Dockable(view: View, position: String) extends Dockable(view, position)
    25 {
    26   Swing_Thread.require()
    27 
    28 
    29   /* component state -- owned by Swing thread */
    30 
    31   private val identification = Document_ID.make().toString
    32 
    33   private var zoom_factor = 100
    34   private var current_snapshot = Document.State.init.snapshot()
    35   private var current_state = Command.empty.init_state
    36   private var current_output: List[XML.Tree] = Nil
    37   private var current_location: Option[Command] = None
    38   private var current_query: String = ""
    39 
    40   private val FIND_THEOREMS = "find_theorems"
    41 
    42 
    43   /* pretty text area */
    44 
    45   val pretty_text_area = new Pretty_Text_Area(view)
    46   set_content(pretty_text_area)
    47 
    48 
    49   private def handle_resize()
    50   {
    51     Swing_Thread.require()
    52 
    53     pretty_text_area.resize(Rendering.font_family(),
    54       (Rendering.font_size("jedit_font_scale") * zoom_factor / 100).round)
    55   }
    56 
    57   private def handle_output()
    58   {
    59     Swing_Thread.require()
    60   }
    61 
    62   private def clear_overlay()
    63   {
    64     Swing_Thread.require()
    65 
    66     for {
    67       command <- current_location
    68       buffer <- JEdit_Lib.jedit_buffer(command.node_name.node)
    69       model <- PIDE.document_model(buffer)
    70     } model.remove_overlay(command, FIND_THEOREMS, List(identification, current_query))
    71 
    72     current_location = None
    73     current_query = ""
    74   }
    75 
    76   private def apply_query(query: String)
    77   {
    78     Swing_Thread.require()
    79 
    80     clear_overlay()
    81     Document_View(view.getTextArea) match {
    82       case Some(doc_view) =>
    83         val snapshot = doc_view.model.snapshot()
    84         snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match {
    85           case Some(command) =>
    86             current_location = Some(command)
    87             current_query = query
    88             doc_view.model.add_overlay(command, FIND_THEOREMS, List(identification, query))
    89           case None =>
    90         }
    91       case None =>
    92     }
    93   }
    94 
    95   private def locate_query()
    96   {
    97     Swing_Thread.require()
    98 
    99     current_location match {
   100       case Some(command) =>
   101         val snapshot = PIDE.session.snapshot(command.node_name)
   102         val commands = snapshot.node.commands
   103         if (commands.contains(command)) {
   104           val sources = commands.iterator.takeWhile(_ != command).map(_.source)
   105           val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column)
   106           Hyperlink(command.node_name.node, line, column).follow(view)
   107         }
   108       case None =>
   109     }
   110   }
   111 
   112 
   113   /* main actor */
   114 
   115   private val main_actor = actor {
   116     loop {
   117       react {
   118         case _: Session.Global_Options =>
   119           Swing_Thread.later { handle_resize() }
   120         case changed: Session.Commands_Changed =>
   121           current_location match {
   122             case Some(command) if changed.commands.contains(command) =>
   123               Swing_Thread.later { handle_output() }
   124             case _ =>
   125           }
   126         case bad =>
   127           java.lang.System.err.println("Find_Dockable: ignoring bad message " + bad)
   128       }
   129     }
   130   }
   131 
   132   override def init()
   133   {
   134     Swing_Thread.require()
   135 
   136     PIDE.session.global_options += main_actor
   137     PIDE.session.commands_changed += main_actor
   138     handle_resize()
   139   }
   140 
   141   override def exit()
   142   {
   143     Swing_Thread.require()
   144 
   145     PIDE.session.global_options -= main_actor
   146     PIDE.session.commands_changed -= main_actor
   147     delay_resize.revoke()
   148   }
   149 
   150 
   151   /* resize */
   152 
   153   private val delay_resize =
   154     Swing_Thread.delay_first(PIDE.options.seconds("editor_update_delay")) { handle_resize() }
   155 
   156   addComponentListener(new ComponentAdapter {
   157     override def componentResized(e: ComponentEvent) { delay_resize.invoke() }
   158   })
   159 
   160 
   161   /* controls */
   162 
   163   private val query = new HistoryTextArea("isabelle-find-theorems") {
   164     { val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) }
   165     setColumns(25)
   166     setRows(1)
   167   }
   168 
   169   private val query_wrapped = Component.wrap(query)
   170 
   171   private val find = new Button("Find") {
   172     tooltip = "Find theorems meeting specified criteria"
   173     reactions += { case ButtonClicked(_) => apply_query(query.getText) }
   174   }
   175 
   176   private val locate = new Button("Locate") {
   177     tooltip = "Locate context of current query within source text"
   178     reactions += { case ButtonClicked(_) => locate_query() }
   179   }
   180 
   181   private val zoom = new GUI.Zoom_Box(factor => { zoom_factor = factor; handle_resize() }) {
   182     tooltip = "Zoom factor for output font size"
   183   }
   184 
   185   private val controls =
   186     new FlowPanel(FlowPanel.Alignment.Right)(query_wrapped, find, locate, zoom)
   187   add(controls.peer, BorderLayout.NORTH)
   188 }