--- a/src/Tools/jEdit/src/jedit/StateViewDockable.scala Sun Dec 21 21:43:41 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/StateViewDockable.scala Sun Dec 21 21:43:41 2008 +0100
@@ -52,6 +52,7 @@
}
}
+
// copy & paste
(new SelectionActions).install(panel)
@@ -62,12 +63,12 @@
private val fontResolver =
panel.getSharedContext.getFontResolver.asInstanceOf[AWTFontResolver]
- if (Plugin.plugin.viewFont != null)
- fontResolver.setFontMapping("Isabelle", Plugin.plugin.viewFont)
+ if (Plugin.self.font != null)
+ fontResolver.setFontMapping("Isabelle", Plugin.self.font)
- Plugin.plugin.viewFontChanged.add(font => {
- if (Plugin.plugin.viewFont != null)
- fontResolver.setFontMapping("Isabelle", Plugin.plugin.viewFont)
+ Plugin.self.font_changed.add(font => {
+ if (Plugin.self.font != null)
+ fontResolver.setFontMapping("Isabelle", Plugin.self.font)
panel.relayout()
})