isabelle: src/Tools/jEdit/src/symbols_dockable.scala@7116f2634e32 (annotated)

50143 4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols; immler parents: diff changeset	1	/* Title: Tools/jEdit/src/symbols_dockable.scala
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols; immler parents: diff changeset	2	Author: Fabian Immler
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols; immler parents: diff changeset	3
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols; immler parents: diff changeset	4	Dockable window for Symbol Palette.
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols; immler parents: diff changeset	5	*/
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols; immler parents: diff changeset	6
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols; immler parents: diff changeset	7	package isabelle.jedit
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols; immler parents: diff changeset	8
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols; immler parents: diff changeset	9
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols; immler parents: diff changeset	10	import isabelle._
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols; immler parents: diff changeset	11
56755 f29c9e7a3a80 clarified GUI focus; wenzelm parents: 56754 diff changeset	12	import scala.swing.event.{SelectionChanged, ValueChanged}
63874 e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	13	import scala.swing.{Component, Action, Button, TabbedPane, TextField, BorderPanel,
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	14	Label, ScrollPane}
50143 4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols; immler parents: diff changeset	15
63872 7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	16	import org.gjt.sp.jedit.{EditBus, EBComponent, EBMessage, View}
50299 f70b3712040f renamed dockable "Prover Session" to "Theories"; wenzelm parents: 50207 diff changeset	17
f70b3712040f renamed dockable "Prover Session" to "Theories"; wenzelm parents: 50207 diff changeset	18
50143 4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols; immler parents: diff changeset	19	class Symbols_Dockable(view: View, position: String) extends Dockable(view, position)
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols; immler parents: diff changeset	20	{
63870 6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	21	private def font_size: Int =
6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	22	Font_Info.main_size(PIDE.options.real("jedit_font_scale")).round
6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	23
63872 7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	24
63877 b4051d3f4e94 tuned; wenzelm parents: 63874 diff changeset	25	/* abbrevs */
63872 7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	26
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	27	private val abbrevs_panel = new Abbrevs_Panel
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	28
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	29	private val abbrevs_refresh_delay =
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	30	GUI_Thread.delay_last(PIDE.options.seconds("editor_update_delay")) { abbrevs_panel.refresh }
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	31
63873 228a85f1d6af clarified GUI representation of replacement texts with zero or more abbrevs; wenzelm parents: 63872 diff changeset	32	private class Abbrev_Component(txt: String, abbrs: List[String]) extends Button
63870 6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	33	{
63874 e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	34	def update_font { font = GUI.font(size = font_size) }
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	35	update_font
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	36
63873 228a85f1d6af clarified GUI representation of replacement texts with zero or more abbrevs; wenzelm parents: 63872 diff changeset	37	text = "<html>" + HTML.output(Symbol.decode(txt)) + "</html>"
63870 6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	38	action =
6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	39	Action(text) {
6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	40	val text_area = view.getTextArea
63873 228a85f1d6af clarified GUI representation of replacement texts with zero or more abbrevs; wenzelm parents: 63872 diff changeset	41	val (s1, s2) =
228a85f1d6af clarified GUI representation of replacement texts with zero or more abbrevs; wenzelm parents: 63872 diff changeset	42	Completion.split_template(Isabelle_Encoding.maybe_decode(text_area.getBuffer, txt))
228a85f1d6af clarified GUI representation of replacement texts with zero or more abbrevs; wenzelm parents: 63872 diff changeset	43	text_area.setSelectedText(s1 + s2)
63870 6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	44	text_area.moveCaretPosition(text_area.getCaretPosition - s2.length)
6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	45	text_area.requestFocus
6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	46	}
63873 228a85f1d6af clarified GUI representation of replacement texts with zero or more abbrevs; wenzelm parents: 63872 diff changeset	47	tooltip = GUI.tooltip_lines(cat_lines(txt :: abbrs.map(a => "abbrev: " + a)))
63870 6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	48	}
6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	49
6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	50	private class Abbrevs_Panel extends Wrap_Panel
6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	51	{
6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	52	private var abbrevs: Thy_Header.Abbrevs = Nil
6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	53
63872 7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	54	def refresh: Unit = GUI_Thread.require {
63873 228a85f1d6af clarified GUI representation of replacement texts with zero or more abbrevs; wenzelm parents: 63872 diff changeset	55	val abbrevs1 = Isabelle.buffer_syntax(view.getBuffer).getOrElse(Outer_Syntax.empty).abbrevs
228a85f1d6af clarified GUI representation of replacement texts with zero or more abbrevs; wenzelm parents: 63872 diff changeset	56
63870 6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	57	if (abbrevs != abbrevs1) {
6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	58	abbrevs = abbrevs1
6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	59
63873 228a85f1d6af clarified GUI representation of replacement texts with zero or more abbrevs; wenzelm parents: 63872 diff changeset	60	val entries: List[(String, List[String])] =
228a85f1d6af clarified GUI representation of replacement texts with zero or more abbrevs; wenzelm parents: 63872 diff changeset	61	Multi_Map(
228a85f1d6af clarified GUI representation of replacement texts with zero or more abbrevs; wenzelm parents: 63872 diff changeset	62	(for {
228a85f1d6af clarified GUI representation of replacement texts with zero or more abbrevs; wenzelm parents: 63872 diff changeset	63	(abbr, txt0) <- abbrevs
63926 70973a1b4ec0 tuned -- fewer warnings; wenzelm parents: 63877 diff changeset	64	txt = Symbol.encode(txt0)
63873 228a85f1d6af clarified GUI representation of replacement texts with zero or more abbrevs; wenzelm parents: 63872 diff changeset	65	if !Symbol.iterator(txt).
228a85f1d6af clarified GUI representation of replacement texts with zero or more abbrevs; wenzelm parents: 63872 diff changeset	66	forall(s => s.length == 1 && s(0) != Completion.caret_indicator)
228a85f1d6af clarified GUI representation of replacement texts with zero or more abbrevs; wenzelm parents: 63872 diff changeset	67	} yield (txt, abbr)): _*).iterator_list.toList
228a85f1d6af clarified GUI representation of replacement texts with zero or more abbrevs; wenzelm parents: 63872 diff changeset	68
63870 6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	69	contents.clear
63873 228a85f1d6af clarified GUI representation of replacement texts with zero or more abbrevs; wenzelm parents: 63872 diff changeset	70	for ((txt, abbrs) <- entries.sortBy(_._1))
228a85f1d6af clarified GUI representation of replacement texts with zero or more abbrevs; wenzelm parents: 63872 diff changeset	71	contents += new Abbrev_Component(txt, abbrs.filterNot(_ == "").sorted)
63870 6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	72
6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	73	revalidate
6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	74	repaint
6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	75	}
6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	76	}
63872 7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	77
63870 6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	78	refresh
6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	79	}
6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	80
63872 7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	81
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	82	/* symbols */
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	83
62104 fb73c0d7bb37 clarified symbol insertion, depending on buffer encoding; wenzelm parents: 62024 diff changeset	84	private class Symbol_Component(val symbol: String, is_control: Boolean) extends Button
50143 4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols; immler parents: diff changeset	85	{
63874 e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	86	def update_font
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	87	{
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	88	font =
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	89	Symbol.fonts.get(symbol) match {
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	90	case None => GUI.font(size = font_size)
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	91	case Some(font_family) => GUI.font(family = font_family, size = font_size)
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	92	}
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	93	}
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	94	update_font
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	95
50187 b5a09812abc4 special handling of control symbols in Symbols dockable; wenzelm parents: 50186 diff changeset	96	action =
62104 fb73c0d7bb37 clarified symbol insertion, depending on buffer encoding; wenzelm parents: 62024 diff changeset	97	Action(Symbol.decode(symbol)) {
50187 b5a09812abc4 special handling of control symbols in Symbols dockable; wenzelm parents: 50186 diff changeset	98	val text_area = view.getTextArea
62104 fb73c0d7bb37 clarified symbol insertion, depending on buffer encoding; wenzelm parents: 62024 diff changeset	99	if (is_control && HTML.control.isDefinedAt(symbol))
fb73c0d7bb37 clarified symbol insertion, depending on buffer encoding; wenzelm parents: 62024 diff changeset	100	Token_Markup.edit_control_style(text_area, symbol)
fb73c0d7bb37 clarified symbol insertion, depending on buffer encoding; wenzelm parents: 62024 diff changeset	101	else
fb73c0d7bb37 clarified symbol insertion, depending on buffer encoding; wenzelm parents: 62024 diff changeset	102	text_area.setSelectedText(Isabelle_Encoding.maybe_decode(text_area.getBuffer, symbol))
50187 b5a09812abc4 special handling of control symbols in Symbols dockable; wenzelm parents: 50186 diff changeset	103	text_area.requestFocus
b5a09812abc4 special handling of control symbols in Symbols dockable; wenzelm parents: 50186 diff changeset	104	}
56622 891d1b8b64fb clarified tooltip_lines: HTML.encode already takes care of newline (but not space); wenzelm parents: 56609 diff changeset	105	tooltip =
891d1b8b64fb clarified tooltip_lines: HTML.encode already takes care of newline (but not space); wenzelm parents: 56609 diff changeset	106	GUI.tooltip_lines(
891d1b8b64fb clarified tooltip_lines: HTML.encode already takes care of newline (but not space); wenzelm parents: 56609 diff changeset	107	cat_lines(symbol :: Symbol.abbrevs.get_list(symbol).map(a => "abbrev: " + a)))
50143 4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols; immler parents: diff changeset	108	}
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols; immler parents: diff changeset	109
50187 b5a09812abc4 special handling of control symbols in Symbols dockable; wenzelm parents: 50186 diff changeset	110	private class Reset_Component extends Button
b5a09812abc4 special handling of control symbols in Symbols dockable; wenzelm parents: 50186 diff changeset	111	{
b5a09812abc4 special handling of control symbols in Symbols dockable; wenzelm parents: 50186 diff changeset	112	action = Action("Reset") {
b5a09812abc4 special handling of control symbols in Symbols dockable; wenzelm parents: 50186 diff changeset	113	val text_area = view.getTextArea
b5a09812abc4 special handling of control symbols in Symbols dockable; wenzelm parents: 50186 diff changeset	114	Token_Markup.edit_control_style(text_area, "")
b5a09812abc4 special handling of control symbols in Symbols dockable; wenzelm parents: 50186 diff changeset	115	text_area.requestFocus
b5a09812abc4 special handling of control symbols in Symbols dockable; wenzelm parents: 50186 diff changeset	116	}
b5a09812abc4 special handling of control symbols in Symbols dockable; wenzelm parents: 50186 diff changeset	117	tooltip = "Reset control symbols within text"
b5a09812abc4 special handling of control symbols in Symbols dockable; wenzelm parents: 50186 diff changeset	118	}
b5a09812abc4 special handling of control symbols in Symbols dockable; wenzelm parents: 50186 diff changeset	119
63872 7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	120
63877 b4051d3f4e94 tuned; wenzelm parents: 63874 diff changeset	121	/* search */
b4051d3f4e94 tuned; wenzelm parents: 63874 diff changeset	122
b4051d3f4e94 tuned; wenzelm parents: 63874 diff changeset	123	private class Search_Panel extends BorderPanel {
b4051d3f4e94 tuned; wenzelm parents: 63874 diff changeset	124	val search_field = new TextField(10)
b4051d3f4e94 tuned; wenzelm parents: 63874 diff changeset	125	val results_panel = new Wrap_Panel
b4051d3f4e94 tuned; wenzelm parents: 63874 diff changeset	126	layout(search_field) = BorderPanel.Position.North
b4051d3f4e94 tuned; wenzelm parents: 63874 diff changeset	127	layout(new ScrollPane(results_panel)) = BorderPanel.Position.Center
b4051d3f4e94 tuned; wenzelm parents: 63874 diff changeset	128
b4051d3f4e94 tuned; wenzelm parents: 63874 diff changeset	129	val search_space =
b4051d3f4e94 tuned; wenzelm parents: 63874 diff changeset	130	(for (sym <- Symbol.names.keysIterator) yield (sym, Word.lowercase(sym))).toList
b4051d3f4e94 tuned; wenzelm parents: 63874 diff changeset	131	val search_delay =
b4051d3f4e94 tuned; wenzelm parents: 63874 diff changeset	132	GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
b4051d3f4e94 tuned; wenzelm parents: 63874 diff changeset	133	val search_words = Word.explode(Word.lowercase(search_field.text))
b4051d3f4e94 tuned; wenzelm parents: 63874 diff changeset	134	val search_limit = PIDE.options.int("jedit_symbols_search_limit") max 0
b4051d3f4e94 tuned; wenzelm parents: 63874 diff changeset	135	val results =
b4051d3f4e94 tuned; wenzelm parents: 63874 diff changeset	136	for ((sym, s) <- search_space; if search_words.forall(s.contains(_))) yield sym
b4051d3f4e94 tuned; wenzelm parents: 63874 diff changeset	137
b4051d3f4e94 tuned; wenzelm parents: 63874 diff changeset	138	results_panel.contents.clear
b4051d3f4e94 tuned; wenzelm parents: 63874 diff changeset	139	for (sym <- results.take(search_limit))
b4051d3f4e94 tuned; wenzelm parents: 63874 diff changeset	140	results_panel.contents += new Symbol_Component(sym, false)
b4051d3f4e94 tuned; wenzelm parents: 63874 diff changeset	141	if (results.length > search_limit)
b4051d3f4e94 tuned; wenzelm parents: 63874 diff changeset	142	results_panel.contents +=
b4051d3f4e94 tuned; wenzelm parents: 63874 diff changeset	143	new Label("...") { tooltip = "(" + (results.length - search_limit) + " more)" }
b4051d3f4e94 tuned; wenzelm parents: 63874 diff changeset	144	revalidate
b4051d3f4e94 tuned; wenzelm parents: 63874 diff changeset	145	repaint
b4051d3f4e94 tuned; wenzelm parents: 63874 diff changeset	146	}
b4051d3f4e94 tuned; wenzelm parents: 63874 diff changeset	147	search_field.reactions += { case ValueChanged(_) => search_delay.invoke() }
b4051d3f4e94 tuned; wenzelm parents: 63874 diff changeset	148	}
b4051d3f4e94 tuned; wenzelm parents: 63874 diff changeset	149
b4051d3f4e94 tuned; wenzelm parents: 63874 diff changeset	150
63872 7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	151	/* tabs */
63870 6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	152
56756 a18c76b7b299 tuned; wenzelm parents: 56755 diff changeset	153	private val group_tabs: TabbedPane = new TabbedPane {
63870 6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	154	pages += new TabbedPane.Page("abbrevs", abbrevs_panel)
6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	155
50192 22d0f64362a5 tuned -- Symbol.groups already sorted; wenzelm parents: 50191 diff changeset	156	pages ++=
56753 40f8822d6bef misc tuning; wenzelm parents: 56622 diff changeset	157	Symbol.groups.map({ case (group, symbols) =>
50151 5f5e74365f14 capitalize lowercase groups; immler parents: 50146 diff changeset	158	new TabbedPane.Page(group,
53713 bb15972a644d improved layout, with special treatment for ScrollPane; wenzelm parents: 53316 diff changeset	159	new ScrollPane(new Wrap_Panel {
62024 e3e22a5e85f2 clarified meaning of \<^bold> action, depending on group; wenzelm parents: 59391 diff changeset	160	val control = group == "control"
e3e22a5e85f2 clarified meaning of \<^bold> action, depending on group; wenzelm parents: 59391 diff changeset	161	contents ++= symbols.map(new Symbol_Component(_, control))
e3e22a5e85f2 clarified meaning of \<^bold> action, depending on group; wenzelm parents: 59391 diff changeset	162	if (control) contents += new Reset_Component
53713 bb15972a644d improved layout, with special treatment for ScrollPane; wenzelm parents: 53316 diff changeset	163	}), null)
56753 40f8822d6bef misc tuning; wenzelm parents: 56622 diff changeset	164	})
40f8822d6bef misc tuning; wenzelm parents: 56622 diff changeset	165
63877 b4051d3f4e94 tuned; wenzelm parents: 63874 diff changeset	166	val search_panel = new Search_Panel
b4051d3f4e94 tuned; wenzelm parents: 63874 diff changeset	167	val search_page = new TabbedPane.Page("search", search_panel, "Search Symbols")
56755 f29c9e7a3a80 clarified GUI focus; wenzelm parents: 56754 diff changeset	168	pages += search_page
f29c9e7a3a80 clarified GUI focus; wenzelm parents: 56754 diff changeset	169
f29c9e7a3a80 clarified GUI focus; wenzelm parents: 56754 diff changeset	170	listenTo(selection)
f29c9e7a3a80 clarified GUI focus; wenzelm parents: 56754 diff changeset	171	reactions += {
63877 b4051d3f4e94 tuned; wenzelm parents: 63874 diff changeset	172	case SelectionChanged(_) if selection.page == search_page =>
b4051d3f4e94 tuned; wenzelm parents: 63874 diff changeset	173	search_panel.search_field.requestFocus
56755 f29c9e7a3a80 clarified GUI focus; wenzelm parents: 56754 diff changeset	174	}
f29c9e7a3a80 clarified GUI focus; wenzelm parents: 56754 diff changeset	175
56756 a18c76b7b299 tuned; wenzelm parents: 56755 diff changeset	176	for (page <- pages)
a18c76b7b299 tuned; wenzelm parents: 56755 diff changeset	177	page.title = Word.implode(Word.explode('_', page.title).map(Word.perhaps_capitalize(_)))
50143 4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols; immler parents: diff changeset	178	}
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols; immler parents: diff changeset	179	set_content(group_tabs)
63872 7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	180
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	181
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	182
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	183	/* main */
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	184
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	185	private val edit_bus_handler: EBComponent =
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	186	new EBComponent { def handleMessage(msg: EBMessage) { abbrevs_refresh_delay.invoke() } }
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	187
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	188	private val main =
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	189	Session.Consumer[Any](getClass.getName) {
63874 e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	190	case _: Session.Global_Options =>
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	191	GUI_Thread.later {
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	192	val comp = group_tabs.peer
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	193	GUI.traverse_components(comp,
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	194	{
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	195	case c0: javax.swing.JComponent =>
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	196	Component.wrap(c0) match {
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	197	case c: Abbrev_Component => c.update_font
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	198	case c: Symbol_Component => c.update_font
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	199	case _ =>
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	200	}
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	201	case _ =>
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	202	})
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	203	comp.revalidate
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	204	comp.repaint()
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	205	}
63872 7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	206	case _: Session.Commands_Changed => abbrevs_refresh_delay.invoke()
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	207	}
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	208
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	209	override def init()
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	210	{
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	211	EditBus.addToBus(edit_bus_handler)
63874 e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	212	PIDE.session.global_options += main
63872 7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	213	PIDE.session.commands_changed += main
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	214	}
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	215
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	216	override def exit()
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	217	{
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	218	EditBus.removeFromBus(edit_bus_handler)
63874 e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	219	PIDE.session.global_options -= main
63872 7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	220	PIDE.session.commands_changed -= main
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	221	}
50143 4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols; immler parents: diff changeset	222	}

author	wenzelm
	Tue, 20 Dec 2016 21:35:56 +0100
changeset 64621	7116f2634e32
parent 63926	70973a1b4ec0
child 65259	41d12227d5dc
permissions	-rw-r--r--