# HG changeset patch
# User wenzelm
# Date 1308663807 -7200
# Node ID 7b7baa28343487c321d9a191d63b06538ff7edd1
# Parent  5e6f76cacb93ba9e00b040aa63a630f1ba36f9f0
hidden font: full height makes cursor more visible;

diff -r 5e6f76cacb93 -r 7b7baa283434 src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Tue Jun 21 14:12:49 2011 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Tue Jun 21 15:43:27 2011 +0200
@@ -10,7 +10,8 @@
 import isabelle._
 
 import java.awt.{Font, Color}
-import java.awt.font.TextAttribute
+import java.awt.font.{TextAttribute, TransformAttribute}
+import java.awt.geom.AffineTransform
 
 import org.gjt.sp.util.SyntaxUtilities
 import org.gjt.sp.jedit.Mode
@@ -47,6 +48,15 @@
   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)
@@ -67,8 +77,7 @@
             font_style(style, font => new Font(family, font.getStyle, font.getSize))
         }
       }
-      new_styles(hidden) =
-        new SyntaxStyle(Color.white, null, new Font(styles(0).getFont.getFamily, 0, 1))
+      new_styles(hidden) = new SyntaxStyle(Color.white, null, hidden_font(styles(0).getFont))
       new_styles
     }
   }