# HG changeset patch # User wenzelm # Date 1473878837 -7200 # Node ID e2393cfde472fb1210b80b4f52d5260308890c7d # Parent 228a85f1d6aff34eaa3a4f68c9c4bc9e08fd82f4 handle font-size events; diff -r 228a85f1d6af -r e2393cfde472 src/Pure/GUI/gui.scala --- a/src/Pure/GUI/gui.scala Wed Sep 14 19:44:08 2016 +0200 +++ b/src/Pure/GUI/gui.scala Wed Sep 14 20:47:17 2016 +0200 @@ -211,6 +211,21 @@ case _ => None } + def traverse_components(component: Component, apply: Component => Unit) + { + def traverse(comp: Component) + { + apply(comp) + comp match { + case cont: Container => + for (i <- 0 until cont.getComponentCount) + traverse(cont.getComponent(i)) + case _ => + } + } + traverse(component) + } + /* font operations */ diff -r 228a85f1d6af -r e2393cfde472 src/Tools/jEdit/src/symbols_dockable.scala --- a/src/Tools/jEdit/src/symbols_dockable.scala Wed Sep 14 19:44:08 2016 +0200 +++ b/src/Tools/jEdit/src/symbols_dockable.scala Wed Sep 14 20:47:17 2016 +0200 @@ -10,7 +10,8 @@ import isabelle._ import scala.swing.event.{SelectionChanged, ValueChanged} -import scala.swing.{Action, Button, TabbedPane, TextField, BorderPanel, Label, ScrollPane} +import scala.swing.{Component, Action, Button, TabbedPane, TextField, BorderPanel, + Label, ScrollPane} import org.gjt.sp.jedit.{EditBus, EBComponent, EBMessage, View} @@ -30,8 +31,10 @@ private class Abbrev_Component(txt: String, abbrs: List[String]) extends Button { + def update_font { font = GUI.font(size = font_size) } + update_font + text = "" + HTML.output(Symbol.decode(txt)) + "" - font = GUI.font(size = font_size) action = Action(text) { val text_area = view.getTextArea @@ -80,11 +83,16 @@ private class Symbol_Component(val symbol: String, is_control: Boolean) extends Button { - font = - Symbol.fonts.get(symbol) match { - case None => GUI.font(size = font_size) - case Some(font_family) => GUI.font(family = font_family, size = font_size) - } + def update_font + { + font = + Symbol.fonts.get(symbol) match { + case None => GUI.font(size = font_size) + case Some(font_family) => GUI.font(family = font_family, size = font_size) + } + } + update_font + action = Action(Symbol.decode(symbol)) { val text_area = view.getTextArea @@ -131,7 +139,7 @@ val results_panel = new Wrap_Panel layout(search_field) = BorderPanel.Position.North layout(new ScrollPane(results_panel)) = BorderPanel.Position.Center - + val search_space = (for (sym <- Symbol.names.keysIterator) yield (sym, Word.lowercase(sym))).toList val search_delay = @@ -173,18 +181,36 @@ private val main = Session.Consumer[Any](getClass.getName) { + case _: Session.Global_Options => + GUI_Thread.later { + val comp = group_tabs.peer + GUI.traverse_components(comp, + { + case c0: javax.swing.JComponent => + Component.wrap(c0) match { + case c: Abbrev_Component => c.update_font + case c: Symbol_Component => c.update_font + case _ => + } + case _ => + }) + comp.revalidate + comp.repaint() + } case _: Session.Commands_Changed => abbrevs_refresh_delay.invoke() } override def init() { EditBus.addToBus(edit_bus_handler) + PIDE.session.global_options += main PIDE.session.commands_changed += main } override def exit() { EditBus.removeFromBus(edit_bus_handler) + PIDE.session.global_options -= main PIDE.session.commands_changed -= main } }