# HG changeset patch
# User wenzelm
# Date 1379867782 -7200
# Node ID e64edcc2f8bf94063aea3b34a400af6a95c89ffb
# Parent  322a3ff42b33f56d91ea6c23f303b4dc1fd0ea99
tuned signature;

diff -r 322a3ff42b33 -r e64edcc2f8bf src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala	Sun Sep 22 18:07:34 2013 +0200
+++ b/src/Pure/GUI/gui.scala	Sun Sep 22 18:36:22 2013 +0200
@@ -7,7 +7,9 @@
 package isabelle
 
 
-import java.awt.{Image, Component, Container, Toolkit, Window}
+import java.awt.{Image, Component, Container, Toolkit, Window, Font}
+import java.awt.font.{TextAttribute, TransformAttribute, FontRenderContext, LineMetrics}
+import java.awt.geom.AffineTransform
 import javax.swing.{ImageIcon, JOptionPane, UIManager, JLayeredPane, JFrame, JWindow}
 
 import scala.swing.{ComboBox, TextArea, ScrollPane}
@@ -150,5 +152,23 @@
       case Some(frame: JFrame) => Some(frame.getLayeredPane)
       case _ => None
     }
+
+
+  /* font operations */
+
+  def font_metrics(font: Font): LineMetrics =
+    font.getLineMetrics("", new FontRenderContext(null, false, false))
+
+  def imitate_font(family: String, font: Font): Font =
+  {
+    val font1 = new Font(family, font.getStyle, font.getSize)
+    font1.deriveFont(font_metrics(font).getAscent / font_metrics(font1).getAscent * font.getSize)
+  }
+
+  def transform_font(font: Font, transform: AffineTransform): Font =
+  {
+    import scala.collection.JavaConversions._
+    font.deriveFont(Map(TextAttribute.TRANSFORM -> new TransformAttribute(transform)))
+  }
 }
 
diff -r 322a3ff42b33 -r e64edcc2f8bf src/Tools/jEdit/src/find_dockable.scala
--- a/src/Tools/jEdit/src/find_dockable.scala	Sun Sep 22 18:07:34 2013 +0200
+++ b/src/Tools/jEdit/src/find_dockable.scala	Sun Sep 22 18:36:22 2013 +0200
@@ -117,7 +117,7 @@
     { val max = getPreferredSize; max.width = Integer.MAX_VALUE; setMaximumSize(max) }
     setColumns(40)
     setToolTipText(query_label.tooltip)
-    setFont(Token_Markup.imitate_font(Rendering.font_family(), getFont))
+    setFont(GUI.imitate_font(Rendering.font_family(), getFont))
   }
 
   private case class Context_Entry(val name: String, val description: String)
diff -r 322a3ff42b33 -r e64edcc2f8bf src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Sun Sep 22 18:07:34 2013 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Sun Sep 22 18:36:22 2013 +0200
@@ -10,7 +10,7 @@
 import isabelle._
 
 import java.awt.{Font, Color}
-import java.awt.font.{TextAttribute, TransformAttribute, FontRenderContext, LineMetrics}
+import java.awt.font.TextAttribute
 import java.awt.geom.AffineTransform
 
 import org.gjt.sp.util.SyntaxUtilities
@@ -68,24 +68,6 @@
   }
 
 
-  /* font operations */
-
-  private def font_metrics(font: Font): LineMetrics =
-    font.getLineMetrics("", new FontRenderContext(null, false, false))
-
-  def imitate_font(family: String, font: Font): Font =
-  {
-    val font1 = new Font(family, font.getStyle, font.getSize)
-    font1.deriveFont(font_metrics(font).getAscent / font_metrics(font1).getAscent * font.getSize)
-  }
-
-  def transform_font(font: Font, transform: AffineTransform): Font =
-  {
-    import scala.collection.JavaConversions._
-    font.deriveFont(Map(TextAttribute.TRANSFORM -> new TransformAttribute(transform)))
-  }
-
-
   /* extended syntax styles */
 
   private val plain_range: Int = JEditToken.ID_COUNT
@@ -109,10 +91,10 @@
         val font1 = font0.deriveFont(Map(TextAttribute.SUPERSCRIPT -> new java.lang.Integer(i)))
 
         def shift(y: Float): Font =
-          transform_font(font1, AffineTransform.getTranslateInstance(0.0, y.toDouble))
+          GUI.transform_font(font1, AffineTransform.getTranslateInstance(0.0, y.toDouble))
 
-        val m0 = font_metrics(font0)
-        val m1 = font_metrics(font1)
+        val m0 = GUI.font_metrics(font0)
+        val m1 = GUI.font_metrics(font1)
         val a = m1.getAscent - m0.getAscent
         val b = (m1.getDescent + m1.getLeading) - (m0.getDescent + m0.getLeading)
         if (a > 0.0f) shift(a)
@@ -145,12 +127,12 @@
         for (idx <- 0 until max_user_fonts)
           new_styles(user_font(idx, i.toByte)) = style
         for ((family, idx) <- Symbol.font_index)
-          new_styles(user_font(idx, i.toByte)) = font_style(style, imitate_font(family, _))
+          new_styles(user_font(idx, i.toByte)) = font_style(style, GUI.imitate_font(family, _))
       }
       new_styles(hidden) =
         new SyntaxStyle(hidden_color, null,
           { val font = styles(0).getFont
-            transform_font(new Font(font.getFamily, 0, 1),
+            GUI.transform_font(new Font(font.getFamily, 0, 1),
               AffineTransform.getScaleInstance(1.0, font.getSize.toDouble)) })
       new_styles
     }