highlight bad range of nested error (here from inner parsing);

--- a/src/Pure/General/markup.ML	Tue Sep 07 15:03:59 2010 +0200
+++ b/src/Pure/General/markup.ML	Tue Sep 07 16:08:29 2010 +0200
@@ -120,6 +120,7 @@
   val promptN: string val prompt: T
   val readyN: string val ready: T
   val reportN: string val report: T
+  val badN: string val bad: T
   val no_output: output * output
   val default_output: T -> output * output
   val add_mode: string -> (T -> output * output) -> unit
@@ -348,6 +349,8 @@
 
 val (reportN, report) = markup_elem "report";
 
+val (badN, bad) = markup_elem "bad";
+
 
 
 (** print mode operations **)

--- a/src/Pure/General/markup.scala	Tue Sep 07 15:03:59 2010 +0200
+++ b/src/Pure/General/markup.scala	Tue Sep 07 16:08:29 2010 +0200
@@ -249,6 +249,8 @@
   val SIGNAL = "signal"
   val EXIT = "exit"
 
+  val BAD = "bad"
+
   val Ready = Markup("ready", Nil)
 
 

--- a/src/Pure/Isar/proof_context.ML	Tue Sep 07 15:03:59 2010 +0200
+++ b/src/Pure/Isar/proof_context.ML	Tue Sep 07 16:08:29 2010 +0200
@@ -736,18 +736,22 @@
 
 local
 
+fun parse_failed ctxt pos msg kind =
+ (Context_Position.report ctxt Markup.bad pos;
+  cat_error msg ("Failed to parse " ^ kind));
+
 fun parse_sort ctxt text =
   let
     val (syms, pos) = Syntax.parse_token ctxt Markup.sort text;
     val S = Syntax.standard_parse_sort ctxt (syn_of ctxt) (syms, pos)
-      handle ERROR msg => cat_error msg "Failed to parse sort";
+      handle ERROR msg => parse_failed ctxt pos msg "sort";
   in Type.minimize_sort (tsig_of ctxt) S end;
 
 fun parse_typ ctxt text =
   let
     val (syms, pos) = Syntax.parse_token ctxt Markup.typ text;
     val T = Syntax.standard_parse_typ ctxt (syn_of ctxt) (get_sort ctxt) (syms, pos)
-      handle ERROR msg => cat_error msg "Failed to parse type";
+      handle ERROR msg => parse_failed ctxt pos msg "type";
   in T end;
 
 fun parse_term T ctxt text =
@@ -764,7 +768,7 @@
     val t =
       Syntax.standard_parse_term check get_sort map_const map_free
         ctxt (Type.is_logtype (tsig_of ctxt)) (syn_of ctxt) T' (syms, pos)
-      handle ERROR msg => cat_error msg ("Failed to parse " ^ kind);
+      handle ERROR msg => parse_failed ctxt pos msg kind;
   in t end;
 
 

--- a/src/Tools/jEdit/src/jedit/document_view.scala	Tue Sep 07 15:03:59 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Tue Sep 07 16:08:29 2010 +0200
@@ -33,6 +33,7 @@
   val regular_color = new Color(192, 192, 192)
   val warning_color = new Color(255, 165, 0)
   val error_color = new Color(255, 106, 106)
+  val bad_color = new Color(255, 204, 153, 100)
 
   def status_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
   {
@@ -67,6 +68,11 @@
     case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
   }
 
+  val background_markup: PartialFunction[Text.Info[Any], Color] =
+  {
+    case Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _)) => bad_color
+  }
+
   val box_markup: PartialFunction[Text.Info[Any], Color] =
   {
     case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => regular_color
@@ -246,7 +252,7 @@
             if (physical_lines(i) != -1) {
               val line_range = proper_line_range(start(i), end(i))
 
-              // background color
+              // background color: status
               val cmds = snapshot.node.command_range(snapshot.revert(line_range))
               for {
                 (command, command_start) <- cmds if !command.is_ignored
@@ -258,6 +264,17 @@
                 gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
               }
 
+              // background color: markup
+              for {
+                Text.Info(range, color) <-
+                  snapshot.select_markup(line_range)(Document_View.background_markup)(null)
+                if color != null
+                r <- Isabelle.gfx_range(text_area, range)
+              } {
+                gfx.setColor(color)
+                gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
+              }
+
               // subexpression highlighting -- potentially from other snapshot
               if (highlight_range.isDefined) {
                 if (line_range.overlaps(highlight_range.get)) {