--- 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] =