--- 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 */
--- 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>" + HTML.output(Symbol.decode(txt)) + "</html>"
- 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
}
}