# HG changeset patch
# User wenzelm
# Date 1308684876 -7200
# Node ID 736183a22fa4b2e9c7a954a5c69d0b3767a82ec0
# Parent  0e422a84d0b25d1158ad671357fc5d586b83d55a
more precise font transformations: shift sub/superscript, adjust size for user fonts;
tuned;

diff -r 0e422a84d0b2 -r 736183a22fa4 src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Tue Jun 21 17:17:39 2011 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Tue Jun 21 21:34:36 2011 +0200
@@ -10,7 +10,7 @@
 import isabelle._
 
 import java.awt.{Font, Color}
-import java.awt.font.{TextAttribute, TransformAttribute}
+import java.awt.font.{TextAttribute, TransformAttribute, FontRenderContext, LineMetrics}
 import java.awt.geom.AffineTransform
 
 import org.gjt.sp.util.SyntaxUtilities
@@ -23,6 +23,24 @@
 
 object Token_Markup
 {
+  /* font operations */
+
+  private def font_metrics(font: Font): LineMetrics =
+    font.getLineMetrics("", new FontRenderContext(null, false, false))
+
+  private 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)
+  }
+
+  private 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
@@ -40,23 +58,27 @@
 
   private def script_style(style: SyntaxStyle, i: Int): SyntaxStyle =
   {
-    import scala.collection.JavaConversions._
-    font_style(style, font =>
-      style.getFont.deriveFont(Map(TextAttribute.SUPERSCRIPT -> new java.lang.Integer(i))))
+    font_style(style, font0 =>
+      {
+        import scala.collection.JavaConversions._
+        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))
+
+        val m0 = font_metrics(font0)
+        val m1 = 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)
+        else if (b > 0.0f) shift(- b)
+        else font1
+      })
   }
 
   private def bold_style(style: SyntaxStyle): SyntaxStyle =
     font_style(style, _.deriveFont(Font.BOLD))
 
-  private def hidden_font(font: Font): Font =
-  {
-    import scala.collection.JavaConversions._
-    val base_font = new Font(font.getFamily, 0, 1)
-    val transform =
-      new TransformAttribute(AffineTransform.getScaleInstance(1.0, font.getSize.toDouble))
-    base_font.deriveFont(Map(TextAttribute.TRANSFORM -> transform))
-  }
-
   class Style_Extender(symbols: Symbol.Interpretation) extends SyntaxUtilities.StyleExtender
   {
     if (symbols.font_names.length > 2)
@@ -71,13 +93,14 @@
         new_styles(subscript(i.toByte)) = script_style(style, -1)
         new_styles(superscript(i.toByte)) = script_style(style, 1)
         new_styles(bold(i.toByte)) = bold_style(style)
-        for ((family, idx) <- symbols.font_index) {
-          // FIXME adjust size
-          new_styles(user_font(idx, i.toByte)) =
-            font_style(style, font => new Font(family, font.getStyle, font.getSize))
-        }
+        for ((family, idx) <- symbols.font_index)
+          new_styles(user_font(idx, i.toByte)) = font_style(style, imitate_font(family, _))
       }
-      new_styles(hidden) = new SyntaxStyle(Color.white, null, hidden_font(styles(0).getFont))
+      new_styles(hidden) =
+        new SyntaxStyle(Color.white, null,
+          { val font = styles(0).getFont
+            transform_font(new Font(font.getFamily, 0, 1),
+              AffineTransform.getScaleInstance(1.0, font.getSize.toDouble)) })
       new_styles
     }
   }