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