# HG changeset patch # User wenzelm # Date 1447103764 -3600 # Node ID a99125aa964f4819b24933d2a8656cfde8f3d465 # Parent 6d5213bd9709ffd2d797b81eb7b0575fadc5bab7 prefer static Font -- evade spontaneous change of TextField.font seen with Metal L&F in Plugin Options / Isabelle / General / Apply; diff -r 6d5213bd9709 -r a99125aa964f src/Tools/jEdit/src/jedit_options.scala --- a/src/Tools/jEdit/src/jedit_options.scala Mon Nov 09 21:04:49 2015 +0100 +++ b/src/Tools/jEdit/src/jedit_options.scala Mon Nov 09 22:16:04 2015 +0100 @@ -9,7 +9,7 @@ import isabelle._ -import java.awt.Color +import java.awt.{Font, Color} import javax.swing.{InputVerifier, JComponent, UIManager} import javax.swing.text.JTextComponent @@ -91,7 +91,8 @@ val default_font = UIManager.getFont("TextField.font") val text_area = new TextArea with Option_Component { - if (default_font != null) font = default_font + if (default_font != null) font = + new Font(default_font.getFamily, default_font.getStyle, default_font.getSize) name = opt_name val title = opt_title def load = text = value.check_name(opt_name).value