# 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))