src/Tools/jEdit/src/symbols_dockable.scala
author wenzelm
Sun Sep 22 18:42:18 2013 +0200 (2013-09-22)
changeset 53786 064cb0458071
parent 53713 bb15972a644d
child 55825 694833e3e4a0
permissions -rw-r--r--
tuned;
     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, TabbedPane, TextField, BorderPanel, Label, ScrollPane}
    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_Font(size = font_size)
    34         case Some(font_family) => Isabelle_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 = GUI.tooltip_lines(symbol :: Symbol.abbrevs.get_list(symbol).map(a => "abbrev: " + a))
    45   }
    46 
    47   private class Reset_Component extends Button
    48   {
    49     action = Action("Reset") {
    50       val text_area = view.getTextArea
    51       Token_Markup.edit_control_style(text_area, "")
    52       text_area.requestFocus
    53     }
    54     tooltip = "Reset control symbols within text"
    55   }
    56 
    57   val group_tabs: TabbedPane = new TabbedPane {
    58     pages ++=
    59       Symbol.groups map { case (group, symbols) =>
    60         new TabbedPane.Page(group,
    61           new ScrollPane(new Wrap_Panel {
    62             contents ++= symbols.map(new Symbol_Component(_))
    63             if (group == "control") contents += new Reset_Component
    64           }), null)
    65       }
    66     pages += new TabbedPane.Page("search", new BorderPanel {
    67       val search = new TextField(10)
    68       val results_panel = new Wrap_Panel
    69       add(search, BorderPanel.Position.North)
    70       add(new ScrollPane(results_panel), BorderPanel.Position.Center)
    71       listenTo(search)
    72       val delay_search =
    73         Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
    74           val max_results = PIDE.options.int("jedit_symbols_search_limit") max 0
    75           results_panel.contents.clear
    76           val results =
    77             (searchspace filter
    78               (Library.lowercase(search.text).split("\\s+") forall _._2.contains)
    79               take (max_results + 1)).toList
    80           for ((sym, _) <- results)
    81             results_panel.contents += new Symbol_Component(sym)
    82           if (results.length > max_results) results_panel.contents += new Label("...")
    83           revalidate
    84           repaint
    85         }
    86       reactions += { case ValueChanged(`search`) => delay_search.invoke() }
    87     }, "Search Symbols")
    88     pages map (p => p.title = (space_explode('_', p.title) map Library.capitalize).mkString(" ") )
    89   }
    90   set_content(group_tabs)
    91 }