# HG changeset patch
# User wenzelm
# Date 1326399682 -3600
# Node ID e4da482283ef2169b223e597a5b2af86444de717
# Parent  805de058722bbb49bc762fc35eb55f638a89ca9d
tuned text_color: cumulate with explicit default color;

diff -r 805de058722b -r e4da482283ef src/Tools/jEdit/src/isabelle_rendering.scala
--- a/src/Tools/jEdit/src/isabelle_rendering.scala	Thu Jan 12 20:58:17 2012 +0100
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Thu Jan 12 21:21:22 2012 +0100
@@ -205,10 +205,11 @@
 
   private val text_color_elements = Set.empty[String] ++ text_colors.keys
 
-  def text_color(snapshot: Document.Snapshot, range: Text.Range): Stream[Text.Info[Option[Color]]] =
-    snapshot.select_markup(range, Some(text_color_elements),
+  def text_color(snapshot: Document.Snapshot, 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, _), _))
+        case (_, Text.Info(_, XML.Elem(Markup(m, _), _)))
         if text_colors.isDefinedAt(m) => text_colors(m)
       })
 
diff -r 805de058722b -r e4da482283ef src/Tools/jEdit/src/text_area_painter.scala
--- a/src/Tools/jEdit/src/text_area_painter.scala	Thu Jan 12 20:58:17 2012 +0100
+++ b/src/Tools/jEdit/src/text_area_painter.scala	Thu Jan 12 21:21:22 2012 +0100
@@ -200,23 +200,24 @@
 
         val markup =
           for {
-            r1 <- Isabelle_Rendering.text_color(painter_snapshot, chunk_range)
+            r1 <- Isabelle_Rendering.text_color(painter_snapshot, chunk_range, chunk_color)
             r2 <- r1.try_restrict(chunk_range)
           } yield r2
 
         val padded_markup =
           if (markup.isEmpty)
-            Iterator(Text.Info(chunk_range, None))
+            Iterator(Text.Info(chunk_range, chunk_color))
           else
-            Iterator(Text.Info(Text.Range(chunk_range.start, markup.head.range.start), None)) ++
+            Iterator(
+              Text.Info(Text.Range(chunk_range.start, markup.head.range.start), chunk_color)) ++
             markup.iterator ++
-            Iterator(Text.Info(Text.Range(markup.last.range.stop, chunk_range.stop), None))
+            Iterator(Text.Info(Text.Range(markup.last.range.stop, chunk_range.stop), chunk_color))
 
         var x1 = x + w
         gfx.setFont(chunk_font)
-        for (Text.Info(range, info) <- padded_markup if !range.is_singularity) {
+        for (Text.Info(range, color) <- padded_markup if !range.is_singularity) {
           val str = chunk_str.substring(range.start - chunk_offset, range.stop - chunk_offset)
-          gfx.setColor(info.getOrElse(chunk_color))
+          gfx.setColor(color)
 
           range.try_restrict(caret_range) match {
             case Some(r) if !r.is_singularity =>