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