# HG changeset patch
# User wenzelm
# Date 1448304693 -3600
# Node ID fd3b214b0979f5d74a3fceca0892da1557945152
# Parent  adf6dd1d490e57ba47a448735a63110c5e4cedaa
clarified font: GUI defaults might change dynamically;

diff -r adf6dd1d490e -r fd3b214b0979 src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala	Mon Nov 23 18:05:33 2015 +0100
+++ b/src/Pure/GUI/gui.scala	Mon Nov 23 19:51:33 2015 +0100
@@ -215,6 +215,10 @@
 
   /* font operations */
 
+  def copy_font(font: Font): Font =
+    if (font == null) null
+    else new Font(font.getFamily, font.getStyle, font.getSize)
+
   def line_metrics(font: Font): LineMetrics =
     font.getLineMetrics("", new FontRenderContext(null, false, false))
 
diff -r adf6dd1d490e -r fd3b214b0979 src/Tools/jEdit/src/jedit_options.scala
--- a/src/Tools/jEdit/src/jedit_options.scala	Mon Nov 23 18:05:33 2015 +0100
+++ b/src/Tools/jEdit/src/jedit_options.scala	Mon Nov 23 19:51:33 2015 +0100
@@ -88,11 +88,10 @@
           def save = bool(opt_name) = selected
         }
       else {
-        val default_font = UIManager.getFont("TextField.font")
+        val default_font = GUI.copy_font(UIManager.getFont("TextField.font"))
         val text_area =
           new TextArea with Option_Component {
-            if (default_font != null) font =
-              new Font(default_font.getFamily, default_font.getStyle, default_font.getSize)
+            if (default_font != null) font = default_font
             name = opt_name
             val title = opt_title
             def load = text = value.check_name(opt_name).value
diff -r adf6dd1d490e -r fd3b214b0979 src/Tools/jEdit/src/session_build.scala
--- a/src/Tools/jEdit/src/session_build.scala	Mon Nov 23 18:05:33 2015 +0100
+++ b/src/Tools/jEdit/src/session_build.scala	Mon Nov 23 19:51:33 2015 +0100
@@ -45,7 +45,7 @@
       columns = 65
       rows = 24
     }
-    text.font = (new Label).font
+    text.font = GUI.copy_font((new Label).font)
 
     private val scroll_text = new ScrollPane(text)