prefer global default font over IsabelleText of jEdit TextArea;
authorwenzelm
Tue, 11 Sep 2012 11:29:28 +0200
changeset 49252 9e10481dd3c4
parent 49251 cd28155bb7d5
child 49269 7157af98ca55
prefer global default font over IsabelleText of jEdit TextArea;
src/Tools/jEdit/src/jedit_options.scala
--- a/src/Tools/jEdit/src/jedit_options.scala	Tue Sep 11 11:03:59 2012 +0200
+++ b/src/Tools/jEdit/src/jedit_options.scala	Tue Sep 11 11:29:28 2012 +0200
@@ -9,8 +9,9 @@
 
 import isabelle._
 
-import javax.swing.{InputVerifier, JComponent}
+import javax.swing.{InputVerifier, JComponent, UIManager}
 import javax.swing.text.JTextComponent
+
 import scala.swing.{Component, CheckBox, TextArea}
 
 
@@ -40,8 +41,10 @@
           def save = bool(opt_name) = selected
         }
       else {
+        val default_font = UIManager.getFont("TextField.font")
         val text_area =
           new TextArea with Option_Component {
+            if (default_font != null) font = default_font
             val title = opt_title
             def load = text = value.check_name(opt_name).value
             def save = update(value + (opt_name, text))