--- 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
}