1/*  Title:      Tools/jEdit/src/symbols_dockable.scala
2    Author:     Fabian Immler
3
4Dockable window for Symbol Palette.
5*/
6
7package isabelle.jedit
8
9
10import isabelle._
11import isabelle.jedit_base.Dockable
12
13import scala.swing.event.{SelectionChanged, ValueChanged}
14import scala.swing.{Component, Action, Button, TabbedPane, TextField, BorderPanel,
15  Label, ScrollPane}
16
17import org.gjt.sp.jedit.{EditBus, EBComponent, EBMessage, View}
18
19
20class Symbols_Dockable(view: View, position: String) extends Dockable(view, position)
21{
22  private def font_size: Int =
23    Font_Info.main_size(PIDE.options.real("jedit_font_scale")).round
24
25
26  /* abbrevs */
27
28  private val abbrevs_panel = new Abbrevs_Panel
29
30  private val abbrevs_refresh_delay =
31    GUI_Thread.delay_last(PIDE.options.seconds("editor_update_delay")) { abbrevs_panel.refresh }
32
33  private class Abbrev_Component(txt: String, abbrs: List[String]) extends Button
34  {
35    def update_font { font = GUI.font(size = font_size) }
36    update_font
37
38    text = "<html>" + HTML.output(Symbol.decode(txt)) + "</html>"
39    action =
40      Action(text) {
41        val text_area = view.getTextArea
42        val (s1, s2) =
43          Completion.split_template(Isabelle_Encoding.perhaps_decode(text_area.getBuffer, txt))
44        text_area.setSelectedText(s1 + s2)
45        text_area.moveCaretPosition(text_area.getCaretPosition - s2.length)
46        text_area.requestFocus
47      }
48    tooltip = GUI.tooltip_lines(cat_lines(txt :: abbrs.map(a => "abbrev: " + a)))
49  }
50
51  private class Abbrevs_Panel extends Wrap_Panel(Nil, Wrap_Panel.Alignment.Center)
52  {
53    private var abbrevs: Thy_Header.Abbrevs = Nil
54
55    def refresh: Unit = GUI_Thread.require {
56      val abbrevs1 = Isabelle.buffer_syntax(view.getBuffer).getOrElse(Outer_Syntax.empty).abbrevs
57
58      if (abbrevs != abbrevs1) {
59        abbrevs = abbrevs1
60
61        val entries: List[(String, List[String])] =
62          Multi_Map(
63            (for {
64              (abbr, txt0) <- abbrevs
65              txt = Symbol.encode(txt0)
66              if !Symbol.iterator(txt).
67                forall(s => s.length == 1 && s(0) != Completion.caret_indicator)
68            } yield (txt, abbr)): _*).iterator_list.toList
69
70        contents.clear
71        for ((txt, abbrs) <- entries.sortBy(_._1))
72          contents += new Abbrev_Component(txt, abbrs.filterNot(_ == "").sorted)
73
74        revalidate
75        repaint
76      }
77    }
78
79    refresh
80  }
81
82
83  /* symbols */
84
85  private class Symbol_Component(val symbol: String, is_control: Boolean) extends Button
86  {
87    def update_font
88    {
89      font =
90        Symbol.fonts.get(symbol) match {
91          case None => GUI.font(size = font_size)
92          case Some(font_family) => GUI.font(family = font_family, size = font_size)
93        }
94    }
95    update_font
96
97    action =
98      Action(Symbol.decode(symbol)) {
99        val text_area = view.getTextArea
100        if (is_control && HTML.is_control(symbol))
101          Syntax_Style.edit_control_style(text_area, symbol)
102        else
103          text_area.setSelectedText(Isabelle_Encoding.perhaps_decode(text_area.getBuffer, symbol))
104        text_area.requestFocus
105      }
106    tooltip =
107      GUI.tooltip_lines(
108        cat_lines(symbol :: Symbol.abbrevs.get_list(symbol).map(a => "abbrev: " + a)))
109  }
110
111  private class Reset_Component extends Button
112  {
113    action = Action("Reset") {
114      val text_area = view.getTextArea
115      Syntax_Style.edit_control_style(text_area, "")
116      text_area.requestFocus
117    }
118    tooltip = "Reset control symbols within text"
119  }
120
121
122  /* search */
123
124  private class Search_Panel extends BorderPanel {
125    val search_field = new TextField(10)
126    val results_panel = Wrap_Panel(Nil, Wrap_Panel.Alignment.Center)
127    layout(search_field) = BorderPanel.Position.North
128    layout(new ScrollPane(results_panel)) = BorderPanel.Position.Center
129
130    val search_space = for ((sym, _) <- Symbol.codes) yield (sym, Word.lowercase(sym))
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_code.map({ case (group, symbols) =>
158        val control = group == "control"
159        new TabbedPane.Page(group,
160          new ScrollPane(Wrap_Panel(
161            symbols.map(new Symbol_Component(_, control)) :::
162            (if (control) List(new Reset_Component) else Nil),
163            Wrap_Panel.Alignment.Center)), 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}
223