# HG changeset patch
# User wenzelm
# Date 1285340947 -7200
# Node ID 6c6164b37fef33df1a880511711808d6e689a695
# Parent  78b185bf7660230c8b94b5d2aacba82a296bdd2d
some attempts to improve visual appearance of bad text;

diff -r 78b185bf7660 -r 6c6164b37fef src/Tools/jEdit/src/jedit/document_view.scala
--- a/src/Tools/jEdit/src/jedit/document_view.scala	Fri Sep 24 16:17:59 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Fri Sep 24 17:09:07 2010 +0200
@@ -230,14 +230,14 @@
               case _ =>
             }
 
-            // boxed text
+            // 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.drawRect(r.x + 1, y + i * line_height + 1, r.length - 2, line_height - 3)
+              gfx.fillRect(r.x + 1, y + i * line_height + 1, r.length - 2, line_height - 2)
             }
 
             // squiggly underline
diff -r 78b185bf7660 -r 6c6164b37fef src/Tools/jEdit/src/jedit/isabelle_markup.scala
--- a/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Fri Sep 24 16:17:59 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_markup.scala	Fri Sep 24 17:09:07 2010 +0200
@@ -21,10 +21,11 @@
   val outdated_color = new Color(240, 240, 240)
   val unfinished_color = new Color(255, 228, 225)
 
+  val light_color = new Color(240, 240, 240)
   val regular_color = new Color(192, 192, 192)
   val warning_color = new Color(255, 168, 0)
   val error_color = new Color(255, 80, 80)
-  val bad_color = new Color(255, 204, 153, 100)
+  val bad_color = new Color(255, 106, 106, 100)
 
   class Icon(val priority: Int, val icon: javax.swing.Icon)
   {
@@ -96,7 +97,7 @@
 
   val box: Markup_Tree.Select[Color] =
   {
-    case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => regular_color
+    case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
   }
 
   val tooltip: Markup_Tree.Select[String] =