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