src/Tools/jEdit/src/symbols_dockable.scala
author wenzelm
Fri Nov 30 21:30:24 2012 +0100 (2012-11-30)
changeset 50299 f70b3712040f
parent 50207 54be125d8cdc
child 51614 22d1dd43f089
permissions -rw-r--r--
renamed dockable "Prover Session" to "Theories";
more uniform Library.lowercase/uppercase;
     1 /*  Title:      Tools/jEdit/src/symbols_dockable.scala
     2     Author:     Fabian Immler
     3 
     4 Dockable window for Symbol Palette.
     5 */
     6 
     7 package isabelle.jedit
     8 
     9 
    10 import isabelle._
    11 
    12 import java.awt.Font
    13 
    14 import scala.swing.event.ValueChanged
    15 import scala.swing.{Action, Button, FlowPanel, TabbedPane, TextField, BorderPanel, Label}
    16 
    17 import org.gjt.sp.jedit.View
    18 
    19 
    20 class Symbols_Dockable(view: View, position: String) extends Dockable(view, position)
    21 {
    22   val searchspace =
    23     for ((group, symbols) <- Symbol.groups; sym <- symbols)
    24       yield (sym, Library.lowercase(sym))
    25 
    26   private class Symbol_Component(val symbol: String) extends Button
    27   {
    28     private val decoded = Symbol.decode(symbol)
    29     private val font_size = Rendering.font_size("jedit_font_scale").round
    30 
    31     font =
    32       Symbol.fonts.get(symbol) match {
    33         case None => Isabelle_System.get_font(size = font_size)
    34         case Some(font_family) => Isabelle_System.get_font(family = font_family, size = font_size)
    35       }
    36     action =
    37       Action(decoded) {
    38         val text_area = view.getTextArea
    39         if (Token_Markup.is_control_style(decoded))
    40           Token_Markup.edit_control_style(text_area, decoded)
    41         else text_area.setSelectedText(decoded)
    42         text_area.requestFocus
    43       }
    44     tooltip =
    45       JEdit_Lib.wrap_tooltip(
    46         symbol +
    47           (if (Symbol.abbrevs.isDefinedAt(symbol)) "\nabbrev: " + Symbol.abbrevs(symbol) else ""))
    48   }
    49 
    50   private class Reset_Component extends Button
    51   {
    52     action = Action("Reset") {
    53       val text_area = view.getTextArea
    54       Token_Markup.edit_control_style(text_area, "")
    55       text_area.requestFocus
    56     }
    57     tooltip = "Reset control symbols within text"
    58   }
    59 
    60   val group_tabs: TabbedPane = new TabbedPane {
    61     pages ++=
    62       Symbol.groups map { case (group, symbols) =>
    63         new TabbedPane.Page(group,
    64           new FlowPanel {
    65             contents ++= symbols.map(new Symbol_Component(_))
    66             if (group == "control") contents += new Reset_Component
    67           }, null)
    68       }
    69     pages += new TabbedPane.Page("search", new BorderPanel {
    70       val search = new TextField(10)
    71       val results_panel = new FlowPanel
    72       add(search, BorderPanel.Position.North)
    73       add(results_panel, BorderPanel.Position.Center)
    74       listenTo(search)
    75       val delay_search =
    76         Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
    77           val max_results = PIDE.options.int("jedit_symbols_search_limit") max 0
    78           results_panel.contents.clear
    79           val results =
    80             (searchspace filter
    81               (Library.lowercase(search.text).split("\\s+") forall _._2.contains)
    82               take (max_results + 1)).toList
    83           for ((sym, _) <- results)
    84             results_panel.contents += new Symbol_Component(sym)
    85           if (results.length > max_results) results_panel.contents += new Label("...")
    86           revalidate
    87           repaint
    88         }
    89       reactions += { case ValueChanged(`search`) => delay_search.invoke() }
    90     }, "Search Symbols")
    91     pages map (p => p.title = (space_explode('_', p.title) map Library.capitalize).mkString(" ") )
    92   }
    93   set_content(group_tabs)
    94 }