# HG changeset patch
# User wenzelm
# Date 1347355768 -7200
# Node ID 9e10481dd3c40aa240621d9d7e18f409ada5e5bf
# Parent  cd28155bb7d5bd0e683b977f854f8355f44410ab
prefer global default font over IsabelleText of jEdit TextArea;

diff -r cd28155bb7d5 -r 9e10481dd3c4 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))