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