src/Tools/jEdit/src/symbols_dockable.scala
author wenzelm
Mon Jan 09 20:26:59 2017 +0100 (2017-01-09)
changeset 64854 f5aa712e6250
parent 63926 70973a1b4ec0
child 65259 41d12227d5dc
permissions -rw-r--r--
tuned signature;
     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.{Component, Action, Button, TabbedPane, TextField, BorderPanel,
    14   Label, ScrollPane}
    15 
    16 import org.gjt.sp.jedit.{EditBus, EBComponent, EBMessage, View}
    17 
    18 
    19 class Symbols_Dockable(view: View, position: String) extends Dockable(view, position)
    20 {
    21   private def font_size: Int =
    22     Font_Info.main_size(PIDE.options.real("jedit_font_scale")).round
    23 
    24 
    25   /* abbrevs */
    26 
    27   private val abbrevs_panel = new Abbrevs_Panel
    28 
    29   private val abbrevs_refresh_delay =
    30     GUI_Thread.delay_last(PIDE.options.seconds("editor_update_delay")) { abbrevs_panel.refresh }
    31 
    32   private class Abbrev_Component(txt: String, abbrs: List[String]) extends Button
    33   {
    34     def update_font { font = GUI.font(size = font_size) }
    35     update_font
    36 
    37     text = "<html>" + HTML.output(Symbol.decode(txt)) + "</html>"
    38     action =
    39       Action(text) {
    40         val text_area = view.getTextArea
    41         val (s1, s2) =
    42           Completion.split_template(Isabelle_Encoding.maybe_decode(text_area.getBuffer, txt))
    43         text_area.setSelectedText(s1 + s2)
    44         text_area.moveCaretPosition(text_area.getCaretPosition - s2.length)
    45         text_area.requestFocus
    46       }
    47     tooltip = GUI.tooltip_lines(cat_lines(txt :: abbrs.map(a => "abbrev: " + a)))
    48   }
    49 
    50   private class Abbrevs_Panel extends Wrap_Panel
    51   {
    52     private var abbrevs: Thy_Header.Abbrevs = Nil
    53 
    54     def refresh: Unit = GUI_Thread.require {
    55       val abbrevs1 = Isabelle.buffer_syntax(view.getBuffer).getOrElse(Outer_Syntax.empty).abbrevs
    56 
    57       if (abbrevs != abbrevs1) {
    58         abbrevs = abbrevs1
    59 
    60         val entries: List[(String, List[String])] =
    61           Multi_Map(
    62             (for {
    63               (abbr, txt0) <- abbrevs
    64               txt = Symbol.encode(txt0)
    65               if !Symbol.iterator(txt).
    66                 forall(s => s.length == 1 && s(0) != Completion.caret_indicator)
    67             } yield (txt, abbr)): _*).iterator_list.toList
    68 
    69         contents.clear
    70         for ((txt, abbrs) <- entries.sortBy(_._1))
    71           contents += new Abbrev_Component(txt, abbrs.filterNot(_ == "").sorted)
    72 
    73         revalidate
    74         repaint
    75       }
    76     }
    77 
    78     refresh
    79   }
    80 
    81 
    82   /* symbols */
    83 
    84   private class Symbol_Component(val symbol: String, is_control: Boolean) extends Button
    85   {
    86     def update_font
    87     {
    88       font =
    89         Symbol.fonts.get(symbol) match {
    90           case None => GUI.font(size = font_size)
    91           case Some(font_family) => GUI.font(family = font_family, size = font_size)
    92         }
    93     }
    94     update_font
    95 
    96     action =
    97       Action(Symbol.decode(symbol)) {
    98         val text_area = view.getTextArea
    99         if (is_control && HTML.control.isDefinedAt(symbol))
   100           Token_Markup.edit_control_style(text_area, symbol)
   101         else
   102           text_area.setSelectedText(Isabelle_Encoding.maybe_decode(text_area.getBuffer, symbol))
   103         text_area.requestFocus
   104       }
   105     tooltip =
   106       GUI.tooltip_lines(
   107         cat_lines(symbol :: Symbol.abbrevs.get_list(symbol).map(a => "abbrev: " + a)))
   108   }
   109 
   110   private class Reset_Component extends Button
   111   {
   112     action = Action("Reset") {
   113       val text_area = view.getTextArea
   114       Token_Markup.edit_control_style(text_area, "")
   115       text_area.requestFocus
   116     }
   117     tooltip = "Reset control symbols within text"
   118   }
   119 
   120 
   121   /* search */
   122 
   123   private class Search_Panel extends BorderPanel {
   124     val search_field = new TextField(10)
   125     val results_panel = new Wrap_Panel
   126     layout(search_field) = BorderPanel.Position.North
   127     layout(new ScrollPane(results_panel)) = BorderPanel.Position.Center
   128 
   129     val search_space =
   130       (for (sym <- Symbol.names.keysIterator) yield (sym, Word.lowercase(sym))).toList
   131     val search_delay =
   132       GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
   133         val search_words = Word.explode(Word.lowercase(search_field.text))
   134         val search_limit = PIDE.options.int("jedit_symbols_search_limit") max 0
   135         val results =
   136           for ((sym, s) <- search_space; if search_words.forall(s.contains(_))) yield sym
   137 
   138         results_panel.contents.clear
   139         for (sym <- results.take(search_limit))
   140           results_panel.contents += new Symbol_Component(sym, false)
   141         if (results.length > search_limit)
   142           results_panel.contents +=
   143             new Label("...") { tooltip = "(" + (results.length - search_limit) + " more)" }
   144         revalidate
   145         repaint
   146       }
   147       search_field.reactions += { case ValueChanged(_) => search_delay.invoke() }
   148   }
   149 
   150 
   151   /* tabs */
   152 
   153   private val group_tabs: TabbedPane = new TabbedPane {
   154     pages += new TabbedPane.Page("abbrevs", abbrevs_panel)
   155 
   156     pages ++=
   157       Symbol.groups.map({ case (group, symbols) =>
   158         new TabbedPane.Page(group,
   159           new ScrollPane(new Wrap_Panel {
   160             val control = group == "control"
   161             contents ++= symbols.map(new Symbol_Component(_, control))
   162             if (control) contents += new Reset_Component
   163           }), null)
   164       })
   165 
   166     val search_panel = new Search_Panel
   167     val search_page = new TabbedPane.Page("search", search_panel, "Search Symbols")
   168     pages += search_page
   169 
   170     listenTo(selection)
   171     reactions += {
   172       case SelectionChanged(_) if selection.page == search_page =>
   173         search_panel.search_field.requestFocus
   174     }
   175 
   176     for (page <- pages)
   177       page.title = Word.implode(Word.explode('_', page.title).map(Word.perhaps_capitalize(_)))
   178   }
   179   set_content(group_tabs)
   180 
   181 
   182 
   183   /* main */
   184 
   185   private val edit_bus_handler: EBComponent =
   186     new EBComponent { def handleMessage(msg: EBMessage) { abbrevs_refresh_delay.invoke() } }
   187 
   188   private val main =
   189     Session.Consumer[Any](getClass.getName) {
   190       case _: Session.Global_Options =>
   191         GUI_Thread.later {
   192           val comp = group_tabs.peer
   193           GUI.traverse_components(comp,
   194             {
   195               case c0: javax.swing.JComponent =>
   196                 Component.wrap(c0) match {
   197                   case c: Abbrev_Component => c.update_font
   198                   case c: Symbol_Component => c.update_font
   199                   case _ =>
   200                 }
   201               case _ =>
   202             })
   203           comp.revalidate
   204           comp.repaint()
   205         }
   206       case _: Session.Commands_Changed => abbrevs_refresh_delay.invoke()
   207     }
   208 
   209   override def init()
   210   {
   211     EditBus.addToBus(edit_bus_handler)
   212     PIDE.session.global_options += main
   213     PIDE.session.commands_changed += main
   214   }
   215 
   216   override def exit()
   217   {
   218     EditBus.removeFromBus(edit_bus_handler)
   219     PIDE.session.global_options -= main
   220     PIDE.session.commands_changed -= main
   221   }
   222 }