src/Tools/jEdit/src/symbols_dockable.scala
author wenzelm
Wed Jul 23 11:19:24 2014 +0200 (2014-07-23)
changeset 57612 990ffb84489b
parent 56769 8649243d7e91
child 57908 1937603dbdf2
permissions -rw-r--r--
clarified module name: facilitate alternative GUI frameworks;
     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 scala.swing.event.{SelectionChanged, ValueChanged}
    13 import scala.swing.{Action, Button, TabbedPane, TextField, BorderPanel, Label, ScrollPane}
    14 
    15 import org.gjt.sp.jedit.View
    16 
    17 
    18 class Symbols_Dockable(view: View, position: String) extends Dockable(view, position)
    19 {
    20   private class Symbol_Component(val symbol: String) extends Button
    21   {
    22     private val decoded = Symbol.decode(symbol)
    23     private val font_size = Font_Info.main_size(PIDE.options.real("jedit_font_scale")).round
    24 
    25     font =
    26       Symbol.fonts.get(symbol) match {
    27         case None => Isabelle_Font(size = font_size)
    28         case Some(font_family) => Isabelle_Font(family = font_family, size = font_size)
    29       }
    30     action =
    31       Action(decoded) {
    32         val text_area = view.getTextArea
    33         if (Token_Markup.is_control_style(decoded))
    34           Token_Markup.edit_control_style(text_area, decoded)
    35         else text_area.setSelectedText(decoded)
    36         text_area.requestFocus
    37       }
    38     tooltip =
    39       GUI.tooltip_lines(
    40         cat_lines(symbol :: Symbol.abbrevs.get_list(symbol).map(a => "abbrev: " + a)))
    41   }
    42 
    43   private class Reset_Component extends Button
    44   {
    45     action = Action("Reset") {
    46       val text_area = view.getTextArea
    47       Token_Markup.edit_control_style(text_area, "")
    48       text_area.requestFocus
    49     }
    50     tooltip = "Reset control symbols within text"
    51   }
    52 
    53   private val group_tabs: TabbedPane = new TabbedPane {
    54     pages ++=
    55       Symbol.groups.map({ case (group, symbols) =>
    56         new TabbedPane.Page(group,
    57           new ScrollPane(new Wrap_Panel {
    58             contents ++= symbols.map(new Symbol_Component(_))
    59             if (group == "control") contents += new Reset_Component
    60           }), null)
    61       })
    62 
    63     val search_field = new TextField(10)
    64     val search_page =
    65       new TabbedPane.Page("search", new BorderPanel {
    66         val results_panel = new Wrap_Panel
    67         add(search_field, BorderPanel.Position.North)
    68         add(new ScrollPane(results_panel), BorderPanel.Position.Center)
    69   
    70         val search_space =
    71           (for (sym <- Symbol.names.keysIterator) yield (sym, Word.lowercase(sym))).toList
    72         val search_delay =
    73           GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
    74             val search_words = Word.explode(Word.lowercase(search_field.text))
    75             val search_limit = PIDE.options.int("jedit_symbols_search_limit") max 0
    76             val results =
    77               for ((sym, s) <- search_space; if search_words.forall(s.contains(_))) yield sym
    78 
    79             results_panel.contents.clear
    80             for (sym <- results.take(search_limit))
    81               results_panel.contents += new Symbol_Component(sym)
    82             if (results.length > search_limit)
    83               results_panel.contents +=
    84                 new Label("...") { tooltip = "(" + (results.length - search_limit) + " more)" }
    85             revalidate
    86             repaint
    87           }
    88           search_field.reactions += { case ValueChanged(_) => search_delay.invoke() }
    89       }, "Search Symbols")
    90     pages += search_page
    91 
    92     listenTo(selection)
    93     reactions += {
    94       case SelectionChanged(_) if selection.page == search_page => search_field.requestFocus
    95     }
    96 
    97     for (page <- pages)
    98       page.title = Word.implode(Word.explode('_', page.title).map(Word.perhaps_capitalize(_)))
    99   }
   100   set_content(group_tabs)
   101 }