# HG changeset patch
# User wenzelm
# Date 1285422040 -7200
# Node ID fa55cf2c1ae4e649d3e03e78b74b197be6f32115
# Parent  6bb073e0385d2d6b8c74cbe64a54178163302ede
more precise treatment of backgrounds vs. rectangles;

diff -r 6bb073e0385d -r fa55cf2c1ae4 src/Tools/jEdit/src/jedit/document_view.scala
--- a/src/Tools/jEdit/src/jedit/document_view.scala	Sat Sep 25 14:16:59 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Sat Sep 25 15:40:40 2010 +0200
@@ -208,16 +208,26 @@
               gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
             }
 
-            // background color: markup
+            // background color (1): markup
             for {
               Text.Info(range, Some(color)) <-
-                snapshot.select_markup(line_range)(Isabelle_Markup.background).iterator
+                snapshot.select_markup(line_range)(Isabelle_Markup.background1).iterator
               r <- Isabelle.gfx_range(text_area, range)
             } {
               gfx.setColor(color)
               gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
             }
 
+            // background color (2): markup
+            for {
+              Text.Info(range, Some(color)) <-
+                snapshot.select_markup(line_range)(Isabelle_Markup.background2).iterator
+              r <- Isabelle.gfx_range(text_area, range)
+            } {
+              gfx.setColor(color)
+              gfx.fillRect(r.x + 2, y + i * line_height + 2, r.length - 4, line_height - 4)
+            }
+
             // sub-expression highlighting -- potentially from other snapshot
             highlight_range match {
               case Some((range, color)) if line_range.overlaps(range) =>
@@ -225,21 +235,11 @@
                   case None =>
                   case Some(r) =>
                     gfx.setColor(color)
-                    gfx.drawRect(r.x, y + i * line_height, r.length, line_height - 1)
+                    gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
                 }
               case _ =>
             }
 
-            // background boxes
-            for {
-              Text.Info(range, Some(color)) <-
-                snapshot.select_markup(line_range)(Isabelle_Markup.box).iterator
-              r <- Isabelle.gfx_range(text_area, range)
-            } {
-              gfx.setColor(color)
-              gfx.fillRect(r.x + 1, y + i * line_height + 1, r.length - 2, line_height - 2)
-            }
-
             // squiggly underline
             for {
               Text.Info(range, Some(color)) <-
diff -r 6bb073e0385d -r fa55cf2c1ae4 src/Tools/jEdit/src/jedit/isabelle_markup.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Sat Sep 25 14:16:59 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Sat Sep 25 15:40:40 2010 +0200
@@ -90,12 +90,12 @@
     case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_icon
   }
 
-  val background: Markup_Tree.Select[Color] =
+  val background1: Markup_Tree.Select[Color] =
   {
     case Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _)) => bad_color
   }
 
-  val box: Markup_Tree.Select[Color] =
+  val background2: Markup_Tree.Select[Color] =
   {
     case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
   }