# HG changeset patch
# User wenzelm
# Date 1353783404 -3600
# Node ID 94886ebf090f6a48701892c83020c0f382104b2f
# Parent  863b1dfc396c53a2af1f6bd1f5dda7eeda770e7e
retain hidden_color (i.e. transparent white) instead of replacing it by semantic text color, to make control symbols more hidden and avoid "dirty" lines with some fonts;

diff -r 863b1dfc396c -r 94886ebf090f src/Tools/jEdit/src/isabelle_rendering.scala
--- a/src/Tools/jEdit/src/isabelle_rendering.scala	Sat Nov 24 19:01:08 2012 +0100
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Sat Nov 24 19:56:44 2012 +0100
@@ -488,10 +488,12 @@
   def text_color(range: Text.Range, color: Color)
       : Stream[Text.Info[Color]] =
   {
-    snapshot.cumulate_markup(range, color, Some(text_color_elements),
-      {
-        case (_, Text.Info(_, XML.Elem(Markup(m, _), _)))
-        if text_colors.isDefinedAt(m) => text_colors(m)
-      })
+    if (color == Token_Markup.hidden_color) Stream(Text.Info(range, color))
+    else
+      snapshot.cumulate_markup(range, color, Some(text_color_elements),
+        {
+          case (_, Text.Info(_, XML.Elem(Markup(m, _), _)))
+          if text_colors.isDefinedAt(m) => text_colors(m)
+        })
   }
 }
diff -r 863b1dfc396c -r 94886ebf090f src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Sat Nov 24 19:01:08 2012 +0100
+++ b/src/Tools/jEdit/src/token_markup.scala	Sat Nov 24 19:56:44 2012 +0100
@@ -122,7 +122,7 @@
   private def bold_style(style: SyntaxStyle): SyntaxStyle =
     font_style(style, _.deriveFont(Font.BOLD))
 
-  private def hidden_color: Color = new Color(255, 255, 255, 0)
+  val hidden_color: Color = new Color(255, 255, 255, 0)
 
   class Style_Extender extends SyntaxUtilities.StyleExtender
   {