some attempts to improve visual appearance of bad text;
authorwenzelm
Fri, 24 Sep 2010 17:09:07 +0200
changeset 39690 6c6164b37fef
parent 39689 78b185bf7660
child 39691 4ce5f79df87a
some attempts to improve visual appearance of bad text;
src/Tools/jEdit/src/jedit/document_view.scala
src/Tools/jEdit/src/jedit/isabelle_markup.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
--- 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] =