report token range after inner parse error -- often provides important clues about misunderstanding concerning lexical phase;
tuned color;

--- a/src/Pure/General/markup.ML	Tue Sep 07 13:16:45 2010 +0200
+++ b/src/Pure/General/markup.ML	Tue Sep 07 14:08:21 2010 +0200
@@ -58,6 +58,7 @@
   val literalN: string val literal: T
   val inner_stringN: string val inner_string: T
   val inner_commentN: string val inner_comment: T
+  val token_rangeN: string val token_range: T
   val sortN: string val sort: T
   val typN: string val typ: T
   val termN: string val term: T
@@ -239,6 +240,8 @@
 val (inner_stringN, inner_string) = markup_elem "inner_string";
 val (inner_commentN, inner_comment) = markup_elem "inner_comment";
 
+val (token_rangeN, token_range) = markup_elem "token_range";
+
 val (sortN, sort) = markup_elem "sort";
 val (typN, typ) = markup_elem "typ";
 val (termN, term) = markup_elem "term";

--- a/src/Pure/General/markup.scala	Tue Sep 07 13:16:45 2010 +0200
+++ b/src/Pure/General/markup.scala	Tue Sep 07 14:08:21 2010 +0200
@@ -136,6 +136,8 @@
   val LITERAL = "literal"
   val INNER_COMMENT = "inner_comment"
 
+  val TOKEN_RANGE = "token_range"
+
   val SORT = "sort"
   val TYP = "typ"
   val TERM = "term"

--- a/src/Pure/Syntax/lexicon.ML	Tue Sep 07 13:16:45 2010 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Tue Sep 07 14:08:21 2010 +0200
@@ -66,6 +66,7 @@
   val terminals: string list
   val is_terminal: string -> bool
   val report_token: Proof.context -> token -> unit
+  val report_token_range: Proof.context -> token -> unit
   val matching_tokens: token * token -> bool
   val valued_token: token -> bool
   val predef_term: string -> token option
@@ -188,6 +189,11 @@
 fun report_token ctxt (Token (kind, _, (pos, _))) =
   Context_Position.report ctxt (token_kind_markup kind) pos;
 
+fun report_token_range ctxt tok =
+  if is_proper tok
+  then Context_Position.report ctxt Markup.token_range (pos_of_token tok)
+  else ();
+
 
 (* matching_tokens *)
 

--- a/src/Pure/Syntax/syntax.ML	Tue Sep 07 13:16:45 2010 +0200
+++ b/src/Pure/Syntax/syntax.ML	Tue Sep 07 14:08:21 2010 +0200
@@ -709,7 +709,8 @@
     val _ = List.app (Lexicon.report_token ctxt) toks;
 
     val root' = if root <> "prop" andalso is_logtype root then Syn_Ext.logic else root;
-    val pts = Parser.parse ctxt gram root' (filter Lexicon.is_proper toks);
+    val pts = Parser.parse ctxt gram root' (filter Lexicon.is_proper toks)
+      handle ERROR msg => (List.app (Lexicon.report_token_range ctxt) toks; error msg);
     val len = length pts;
 
     val limit = Config.get ctxt ambiguity_limit;

--- a/src/Tools/jEdit/src/jedit/document_view.scala	Tue Sep 07 13:16:45 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Tue Sep 07 14:08:21 2010 +0200
@@ -43,11 +43,16 @@
 
   val message_markup: PartialFunction[Text.Info[Any], Color] =
   {
-    case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => new Color(220, 220, 220)
+    case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => new Color(192, 192, 192)
     case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => new Color(255, 165, 0)
     case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => new Color(255, 106, 106)
   }
 
+  val box_markup: PartialFunction[Text.Info[Any], Color] =
+  {
+    case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => new Color(192, 192, 192)
+  }
+
 
   /* document view of text area */
 
@@ -245,6 +250,17 @@
                 }
               }
 
+              // boxed text
+              for {
+                Text.Info(range, color) <-
+                  snapshot.select_markup(line_range)(Document_View.box_markup)(null)
+                if color != null
+                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)
+              }
+
               // squiggly underline
               for {
                 Text.Info(range, color) <-