isabelle: src/Tools/jEdit/src/symbols_dockable.scala@e2393cfde472 (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
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	25	/* abbreviations */
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
228a85f1d6af clarified GUI representation of replacement texts with zero or more abbrevs; wenzelm parents: 63872 diff changeset	64	val txt = Symbol.encode(txt0)
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
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	121	/* tabs */
63870 6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	122
56756 a18c76b7b299 tuned; wenzelm parents: 56755 diff changeset	123	private val group_tabs: TabbedPane = new TabbedPane {
63870 6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	124	pages += new TabbedPane.Page("abbrevs", abbrevs_panel)
6db1aac936db added abbrevs panel; wenzelm parents: 62104 diff changeset	125
50192 22d0f64362a5 tuned -- Symbol.groups already sorted; wenzelm parents: 50191 diff changeset	126	pages ++=
56753 40f8822d6bef misc tuning; wenzelm parents: 56622 diff changeset	127	Symbol.groups.map({ case (group, symbols) =>
50151 5f5e74365f14 capitalize lowercase groups; immler parents: 50146 diff changeset	128	new TabbedPane.Page(group,
53713 bb15972a644d improved layout, with special treatment for ScrollPane; wenzelm parents: 53316 diff changeset	129	new ScrollPane(new Wrap_Panel {
62024 e3e22a5e85f2 clarified meaning of \<^bold> action, depending on group; wenzelm parents: 59391 diff changeset	130	val control = group == "control"
e3e22a5e85f2 clarified meaning of \<^bold> action, depending on group; wenzelm parents: 59391 diff changeset	131	contents ++= symbols.map(new Symbol_Component(_, control))
e3e22a5e85f2 clarified meaning of \<^bold> action, depending on group; wenzelm parents: 59391 diff changeset	132	if (control) contents += new Reset_Component
53713 bb15972a644d improved layout, with special treatment for ScrollPane; wenzelm parents: 53316 diff changeset	133	}), null)
56753 40f8822d6bef misc tuning; wenzelm parents: 56622 diff changeset	134	})
40f8822d6bef misc tuning; wenzelm parents: 56622 diff changeset	135
56755 f29c9e7a3a80 clarified GUI focus; wenzelm parents: 56754 diff changeset	136	val search_field = new TextField(10)
f29c9e7a3a80 clarified GUI focus; wenzelm parents: 56754 diff changeset	137	val search_page =
f29c9e7a3a80 clarified GUI focus; wenzelm parents: 56754 diff changeset	138	new TabbedPane.Page("search", new BorderPanel {
f29c9e7a3a80 clarified GUI focus; wenzelm parents: 56754 diff changeset	139	val results_panel = new Wrap_Panel
59391 39a38657d16b tuned; wenzelm parents: 59063 diff changeset	140	layout(search_field) = BorderPanel.Position.North
39a38657d16b tuned; wenzelm parents: 59063 diff changeset	141	layout(new ScrollPane(results_panel)) = BorderPanel.Position.Center
63874 e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	142
56755 f29c9e7a3a80 clarified GUI focus; wenzelm parents: 56754 diff changeset	143	val search_space =
f29c9e7a3a80 clarified GUI focus; wenzelm parents: 56754 diff changeset	144	(for (sym <- Symbol.names.keysIterator) yield (sym, Word.lowercase(sym))).toList
56769 8649243d7e91 tuned; wenzelm parents: 56756 diff changeset	145	val search_delay =
57612 990ffb84489b clarified module name: facilitate alternative GUI frameworks; wenzelm parents: 56769 diff changeset	146	GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) {
56756 a18c76b7b299 tuned; wenzelm parents: 56755 diff changeset	147	val search_words = Word.explode(Word.lowercase(search_field.text))
56755 f29c9e7a3a80 clarified GUI focus; wenzelm parents: 56754 diff changeset	148	val search_limit = PIDE.options.int("jedit_symbols_search_limit") max 0
56756 a18c76b7b299 tuned; wenzelm parents: 56755 diff changeset	149	val results =
a18c76b7b299 tuned; wenzelm parents: 56755 diff changeset	150	for ((sym, s) <- search_space; if search_words.forall(s.contains(_))) yield sym
a18c76b7b299 tuned; wenzelm parents: 56755 diff changeset	151
56755 f29c9e7a3a80 clarified GUI focus; wenzelm parents: 56754 diff changeset	152	results_panel.contents.clear
f29c9e7a3a80 clarified GUI focus; wenzelm parents: 56754 diff changeset	153	for (sym <- results.take(search_limit))
62024 e3e22a5e85f2 clarified meaning of \<^bold> action, depending on group; wenzelm parents: 59391 diff changeset	154	results_panel.contents += new Symbol_Component(sym, false)
56755 f29c9e7a3a80 clarified GUI focus; wenzelm parents: 56754 diff changeset	155	if (results.length > search_limit)
56756 a18c76b7b299 tuned; wenzelm parents: 56755 diff changeset	156	results_panel.contents +=
a18c76b7b299 tuned; wenzelm parents: 56755 diff changeset	157	new Label("...") { tooltip = "(" + (results.length - search_limit) + " more)" }
56755 f29c9e7a3a80 clarified GUI focus; wenzelm parents: 56754 diff changeset	158	revalidate
f29c9e7a3a80 clarified GUI focus; wenzelm parents: 56754 diff changeset	159	repaint
f29c9e7a3a80 clarified GUI focus; wenzelm parents: 56754 diff changeset	160	}
56769 8649243d7e91 tuned; wenzelm parents: 56756 diff changeset	161	search_field.reactions += { case ValueChanged(_) => search_delay.invoke() }
56755 f29c9e7a3a80 clarified GUI focus; wenzelm parents: 56754 diff changeset	162	}, "Search Symbols")
f29c9e7a3a80 clarified GUI focus; wenzelm parents: 56754 diff changeset	163	pages += search_page
f29c9e7a3a80 clarified GUI focus; wenzelm parents: 56754 diff changeset	164
f29c9e7a3a80 clarified GUI focus; wenzelm parents: 56754 diff changeset	165	listenTo(selection)
f29c9e7a3a80 clarified GUI focus; wenzelm parents: 56754 diff changeset	166	reactions += {
f29c9e7a3a80 clarified GUI focus; wenzelm parents: 56754 diff changeset	167	case SelectionChanged(_) if selection.page == search_page => search_field.requestFocus
f29c9e7a3a80 clarified GUI focus; wenzelm parents: 56754 diff changeset	168	}
f29c9e7a3a80 clarified GUI focus; wenzelm parents: 56754 diff changeset	169
56756 a18c76b7b299 tuned; wenzelm parents: 56755 diff changeset	170	for (page <- pages)
a18c76b7b299 tuned; wenzelm parents: 56755 diff changeset	171	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	172	}
4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols; immler parents: diff changeset	173	set_content(group_tabs)
63872 7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	174
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	175
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	176
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	177	/* main */
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	178
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	179	private val edit_bus_handler: EBComponent =
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	180	new EBComponent { def handleMessage(msg: EBMessage) { abbrevs_refresh_delay.invoke() } }
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	181
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	182	private val main =
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	183	Session.Consumer[Any](getClass.getName) {
63874 e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	184	case _: Session.Global_Options =>
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	185	GUI_Thread.later {
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	186	val comp = group_tabs.peer
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	187	GUI.traverse_components(comp,
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	188	{
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	189	case c0: javax.swing.JComponent =>
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	190	Component.wrap(c0) match {
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	191	case c: Abbrev_Component => c.update_font
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	192	case c: Symbol_Component => c.update_font
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	193	case _ =>
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	194	}
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	195	case _ =>
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	196	})
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	197	comp.revalidate
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	198	comp.repaint()
e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	199	}
63872 7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	200	case _: Session.Commands_Changed => abbrevs_refresh_delay.invoke()
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	201	}
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	202
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	203	override def init()
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	204	{
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	205	EditBus.addToBus(edit_bus_handler)
63874 e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	206	PIDE.session.global_options += main
63872 7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	207	PIDE.session.commands_changed += main
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	208	}
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	209
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	210	override def exit()
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	211	{
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	212	EditBus.removeFromBus(edit_bus_handler)
63874 e2393cfde472 handle font-size events; wenzelm parents: 63873 diff changeset	213	PIDE.session.global_options -= main
63872 7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	214	PIDE.session.commands_changed -= main
7dd5297d87fa handle update events; wenzelm parents: 63870 diff changeset	215	}
50143 4ff5d795ed08 dockable with buttons for symbols, grouped and sorted in tabs according to ~~/etc/symbols; immler parents: diff changeset	216	}

author	wenzelm
	Wed, 14 Sep 2016 20:47:17 +0200
changeset 63874	e2393cfde472
parent 63873	228a85f1d6af
child 63877	b4051d3f4e94
permissions	-rw-r--r--