changeset 34456 | 14367c0715e8 |
parent 34441 | ff3b7ae2b12a |
child 34552 | 65f1b2261cc6 |
--- a/src/Tools/jEdit/src/jedit/StateViewDockable.scala Mon Dec 29 20:36:34 2008 +0100 +++ b/src/Tools/jEdit/src/jedit/StateViewDockable.scala Mon Dec 29 20:43:04 2008 +0100 @@ -66,7 +66,7 @@ if (Isabelle.plugin.font != null) fontResolver.setFontMapping("Isabelle", Isabelle.plugin.font) - Isabelle.plugin.font_changed.add(font => { + Isabelle.plugin.font_changed += (font => { if (Isabelle.plugin.font != null) fontResolver.setFontMapping("Isabelle", Isabelle.plugin.font)