isabelle: src/Tools/jEdit/src/symbols_dockable.scala@1514efa1e57a (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._
66591 6efa351190d0 more robust: provide docking framework via base plugin; wenzelm parents: 66206 diff changeset	11	import isabelle.jedit_base.Dockable
50143 4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols; immler parents: diff changeset	12
56755 f29c9e7a3a80 clarified GUI focus; wenzelm parents: 56754 diff changeset	13	import scala.swing.event.{SelectionChanged, ValueChanged}
63874 e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	14	import scala.swing.{Component, Action, Button, TabbedPane, TextField, BorderPanel,
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	15	Label, ScrollPane}
50143 4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols; immler parents: diff changeset	16
63872 7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	17	import org.gjt.sp.jedit.{EditBus, EBComponent, EBMessage, View}
50299 f70b3712040f renamed dockable "Prover Session" to "Theories"; wenzelm parents: 50207 diff changeset	18
f70b3712040f renamed dockable "Prover Session" to "Theories"; wenzelm parents: 50207 diff changeset	19
50143 4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols; immler parents: diff changeset	20	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	21	{
63870 6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	22	private def font_size: Int =
6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	23	Font_Info.main_size(PIDE.options.real("jedit_font_scale")).round
6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	24
63872 7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	25
63877 b4051d3f4e94 tuned; wenzelm parents: 63874 diff changeset	26	/* abbrevs */
63872 7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	27
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	28	private val abbrevs_panel = new Abbrevs_Panel
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	29
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	30	private val abbrevs_refresh_delay =
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	31	GUI_Thread.delay_last(PIDE.options.seconds("editor_update_delay")) { abbrevs_panel.refresh }
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	32
63873 228a85f1d6af clarified GUI representation of replacement texts with zero or more abbrevs; wenzelm parents: 63872 diff changeset	33	private class Abbrev_Component(txt: String, abbrs: List[String]) extends Button
63870 6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	34	{
63874 e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	35	def update_font { font = GUI.font(size = font_size) }
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	36	update_font
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	37
63873 228a85f1d6af clarified GUI representation of replacement texts with zero or more abbrevs; wenzelm parents: 63872 diff changeset	38	text = "<html>" + HTML.output(Symbol.decode(txt)) + "</html>"
63870 6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	39	action =
6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	40	Action(text) {
6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	41	val text_area = view.getTextArea
63873 228a85f1d6af clarified GUI representation of replacement texts with zero or more abbrevs; wenzelm parents: 63872 diff changeset	42	val (s1, s2) =
67130 b023f64e0d16 tuned signature; wenzelm parents: 66591 diff changeset	43	Completion.split_template(Isabelle_Encoding.perhaps_decode(text_area.getBuffer, txt))
63873 228a85f1d6af clarified GUI representation of replacement texts with zero or more abbrevs; wenzelm parents: 63872 diff changeset	44	text_area.setSelectedText(s1 + s2)
63870 6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	45	text_area.moveCaretPosition(text_area.getCaretPosition - s2.length)
6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	46	text_area.requestFocus
6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	47	}
63873 228a85f1d6af clarified GUI representation of replacement texts with zero or more abbrevs; wenzelm parents: 63872 diff changeset	48	tooltip = GUI.tooltip_lines(cat_lines(txt :: abbrs.map(a => "abbrev: " + a)))
63870 6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	49	}
6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	50
66206 2d2082db735a clarified defaults; wenzelm parents: 66205 diff changeset	51	private class Abbrevs_Panel extends Wrap_Panel(Nil, Wrap_Panel.Alignment.Center)
63870 6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	52	{
6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	53	private var abbrevs: Thy_Header.Abbrevs = Nil
6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	54
63872 7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	55	def refresh: Unit = GUI_Thread.require {
63873 228a85f1d6af clarified GUI representation of replacement texts with zero or more abbrevs; wenzelm parents: 63872 diff changeset	56	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	57
63870 6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	58	if (abbrevs != abbrevs1) {
6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	59	abbrevs = abbrevs1
6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	60
63873 228a85f1d6af clarified GUI representation of replacement texts with zero or more abbrevs; wenzelm parents: 63872 diff changeset	61	val entries: List[(String, List[String])] =
228a85f1d6af clarified GUI representation of replacement texts with zero or more abbrevs; wenzelm parents: 63872 diff changeset	62	Multi_Map(
228a85f1d6af clarified GUI representation of replacement texts with zero or more abbrevs; wenzelm parents: 63872 diff changeset	63	(for {
228a85f1d6af clarified GUI representation of replacement texts with zero or more abbrevs; wenzelm parents: 63872 diff changeset	64	(abbr, txt0) <- abbrevs
63926 70973a1b4ec0 tuned -- fewer warnings; wenzelm parents: 63877 diff changeset	65	txt = Symbol.encode(txt0)
63873 228a85f1d6af clarified GUI representation of replacement texts with zero or more abbrevs; wenzelm parents: 63872 diff changeset	66	if !Symbol.iterator(txt).
228a85f1d6af clarified GUI representation of replacement texts with zero or more abbrevs; wenzelm parents: 63872 diff changeset	67	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	68	} yield (txt, abbr)): _*).iterator_list.toList
228a85f1d6af clarified GUI representation of replacement texts with zero or more abbrevs; wenzelm parents: 63872 diff changeset	69
63870 6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	70	contents.clear
63873 228a85f1d6af clarified GUI representation of replacement texts with zero or more abbrevs; wenzelm parents: 63872 diff changeset	71	for ((txt, abbrs) <- entries.sortBy(_._1))
228a85f1d6af clarified GUI representation of replacement texts with zero or more abbrevs; wenzelm parents: 63872 diff changeset	72	contents += new Abbrev_Component(txt, abbrs.filterNot(_ == "").sorted)
63870 6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	73
6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	74	revalidate
6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	75	repaint
6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	76	}
6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	77	}
63872 7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	78
63870 6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	79	refresh
6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	80	}
6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	81
63872 7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	82
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	83	/* symbols */
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	84
62104 fb73c0d7bb37 clarified symbol insertion, depending on buffer encoding; wenzelm parents: 62024 diff changeset	85	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	86	{
63874 e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	87	def update_font
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	88	{
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	89	font =
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	90	Symbol.fonts.get(symbol) match {
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	91	case None => GUI.font(size = font_size)
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	92	case Some(font_family) => GUI.font(family = font_family, size = font_size)
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	93	}
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	94	}
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	95	update_font
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	96
50187 b5a09812abc4 special handling of control symbols in Symbols dockable; wenzelm parents: 50186 diff changeset	97	action =
62104 fb73c0d7bb37 clarified symbol insertion, depending on buffer encoding; wenzelm parents: 62024 diff changeset	98	Action(Symbol.decode(symbol)) {
50187 b5a09812abc4 special handling of control symbols in Symbols dockable; wenzelm parents: 50186 diff changeset	99	val text_area = view.getTextArea
65997 e3dc9ea67a62 output control symbols like ML version, with optionally hidden source; wenzelm parents: 65259 diff changeset	100	if (is_control && HTML.is_control(symbol))
65259 41d12227d5dc clarified modules; wenzelm parents: 63926 diff changeset	101	Syntax_Style.edit_control_style(text_area, symbol)
62104 fb73c0d7bb37 clarified symbol insertion, depending on buffer encoding; wenzelm parents: 62024 diff changeset	102	else
67130 b023f64e0d16 tuned signature; wenzelm parents: 66591 diff changeset	103	text_area.setSelectedText(Isabelle_Encoding.perhaps_decode(text_area.getBuffer, symbol))
50187 b5a09812abc4 special handling of control symbols in Symbols dockable; wenzelm parents: 50186 diff changeset	104	text_area.requestFocus
b5a09812abc4 special handling of control symbols in Symbols dockable; wenzelm parents: 50186 diff changeset	105	}
56622 891d1b8b64fb clarified tooltip_lines: HTML.encode already takes care of newline (but not space); wenzelm parents: 56609 diff changeset	106	tooltip =
891d1b8b64fb clarified tooltip_lines: HTML.encode already takes care of newline (but not space); wenzelm parents: 56609 diff changeset	107	GUI.tooltip_lines(
891d1b8b64fb clarified tooltip_lines: HTML.encode already takes care of newline (but not space); wenzelm parents: 56609 diff changeset	108	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	109	}
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols; immler parents: diff changeset	110
50187 b5a09812abc4 special handling of control symbols in Symbols dockable; wenzelm parents: 50186 diff changeset	111	private class Reset_Component extends Button
b5a09812abc4 special handling of control symbols in Symbols dockable; wenzelm parents: 50186 diff changeset	112	{
b5a09812abc4 special handling of control symbols in Symbols dockable; wenzelm parents: 50186 diff changeset	113	action = Action("Reset") {
b5a09812abc4 special handling of control symbols in Symbols dockable; wenzelm parents: 50186 diff changeset	114	val text_area = view.getTextArea
65259 41d12227d5dc clarified modules; wenzelm parents: 63926 diff changeset	115	Syntax_Style.edit_control_style(text_area, "")
50187 b5a09812abc4 special handling of control symbols in Symbols dockable; wenzelm parents: 50186 diff changeset	116	text_area.requestFocus
b5a09812abc4 special handling of control symbols in Symbols dockable; wenzelm parents: 50186 diff changeset	117	}
b5a09812abc4 special handling of control symbols in Symbols dockable; wenzelm parents: 50186 diff changeset	118	tooltip = "Reset control symbols within text"
b5a09812abc4 special handling of control symbols in Symbols dockable; wenzelm parents: 50186 diff changeset	119	}
b5a09812abc4 special handling of control symbols in Symbols dockable; wenzelm parents: 50186 diff changeset	120
63872 7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	121
63877 b4051d3f4e94 tuned; wenzelm parents: 63874 diff changeset	122	/* search */
b4051d3f4e94 tuned; wenzelm parents: 63874 diff changeset	123
b4051d3f4e94 tuned; wenzelm parents: 63874 diff changeset	124	private class Search_Panel extends BorderPanel {
b4051d3f4e94 tuned; wenzelm parents: 63874 diff changeset	125	val search_field = new TextField(10)
66206 2d2082db735a clarified defaults; wenzelm parents: 66205 diff changeset	126	val results_panel = Wrap_Panel(Nil, Wrap_Panel.Alignment.Center)
63877 b4051d3f4e94 tuned; wenzelm parents: 63874 diff changeset	127	layout(search_field) = BorderPanel.Position.North
b4051d3f4e94 tuned; wenzelm parents: 63874 diff changeset	128	layout(new ScrollPane(results_panel)) = BorderPanel.Position.Center
b4051d3f4e94 tuned; wenzelm parents: 63874 diff changeset	129
67389 7e21d19e7ad7 show only symbols with code; wenzelm parents: 67130 diff changeset	130	val search_space = for ((sym, _) <- Symbol.codes) yield (sym, Word.lowercase(sym))
63877 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 ++=
67389 7e21d19e7ad7 show only symbols with code; wenzelm parents: 67130 diff changeset	157	Symbol.groups_code.map({ case (group, symbols) =>
66205 e9fa94f43a15 tuned signature; wenzelm parents: 65997 diff changeset	158	val control = group == "control"
50151 5f5e74365f14 capitalize lowercase groups; immler parents: 50146 diff changeset	159	new TabbedPane.Page(group,
66205 e9fa94f43a15 tuned signature; wenzelm parents: 65997 diff changeset	160	new ScrollPane(Wrap_Panel(
e9fa94f43a15 tuned signature; wenzelm parents: 65997 diff changeset	161	symbols.map(new Symbol_Component(_, control)) :::
66206 2d2082db735a clarified defaults; wenzelm parents: 66205 diff changeset	162	(if (control) List(new Reset_Component) else Nil),
2d2082db735a clarified defaults; wenzelm parents: 66205 diff changeset	163	Wrap_Panel.Alignment.Center)), 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
	Mon, 03 Jun 2019 13:28:01 +0200
changeset 70304	1514efa1e57a
parent 67389	7e21d19e7ad7
child 71601	97ccf48c2f0c
permissions	-rw-r--r--