1.1 --- a/src/Pure/General/markup.ML	Tue Sep 07 13:16:45 2010 +0200
     1.2 +++ b/src/Pure/General/markup.ML	Tue Sep 07 14:08:21 2010 +0200
     1.3 @@ -58,6 +58,7 @@
     1.4    val literalN: string val literal: T
     1.5    val inner_stringN: string val inner_string: T
     1.6    val inner_commentN: string val inner_comment: T
     1.7 +  val token_rangeN: string val token_range: T
     1.8    val sortN: string val sort: T
     1.9    val typN: string val typ: T
    1.10    val termN: string val term: T
    1.11 @@ -239,6 +240,8 @@
    1.12  val (inner_stringN, inner_string) = markup_elem "inner_string";
    1.13  val (inner_commentN, inner_comment) = markup_elem "inner_comment";
    1.14  
    1.15 +val (token_rangeN, token_range) = markup_elem "token_range";
    1.16 +
    1.17  val (sortN, sort) = markup_elem "sort";
    1.18  val (typN, typ) = markup_elem "typ";
    1.19  val (termN, term) = markup_elem "term";

     2.1 --- a/src/Pure/General/markup.scala	Tue Sep 07 13:16:45 2010 +0200
     2.2 +++ b/src/Pure/General/markup.scala	Tue Sep 07 14:08:21 2010 +0200
     2.3 @@ -136,6 +136,8 @@
     2.4    val LITERAL = "literal"
     2.5    val INNER_COMMENT = "inner_comment"
     2.6  
     2.7 +  val TOKEN_RANGE = "token_range"
     2.8 +
     2.9    val SORT = "sort"
    2.10    val TYP = "typ"
    2.11    val TERM = "term"

     3.1 --- a/src/Pure/Syntax/lexicon.ML	Tue Sep 07 13:16:45 2010 +0200
     3.2 +++ b/src/Pure/Syntax/lexicon.ML	Tue Sep 07 14:08:21 2010 +0200
     3.3 @@ -66,6 +66,7 @@
     3.4    val terminals: string list
     3.5    val is_terminal: string -> bool
     3.6    val report_token: Proof.context -> token -> unit
     3.7 +  val report_token_range: Proof.context -> token -> unit
     3.8    val matching_tokens: token * token -> bool
     3.9    val valued_token: token -> bool
    3.10    val predef_term: string -> token option
    3.11 @@ -188,6 +189,11 @@
    3.12  fun report_token ctxt (Token (kind, _, (pos, _))) =
    3.13    Context_Position.report ctxt (token_kind_markup kind) pos;
    3.14  
    3.15 +fun report_token_range ctxt tok =
    3.16 +  if is_proper tok
    3.17 +  then Context_Position.report ctxt Markup.token_range (pos_of_token tok)
    3.18 +  else ();
    3.19 +
    3.20  
    3.21  (* matching_tokens *)
    3.22  

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

     5.1 --- a/src/Tools/jEdit/src/jedit/document_view.scala	Tue Sep 07 13:16:45 2010 +0200
     5.2 +++ b/src/Tools/jEdit/src/jedit/document_view.scala	Tue Sep 07 14:08:21 2010 +0200
     5.3 @@ -43,11 +43,16 @@
     5.4  
     5.5    val message_markup: PartialFunction[Text.Info[Any], Color] =
     5.6    {
     5.7 -    case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => new Color(220, 220, 220)
     5.8 +    case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => new Color(192, 192, 192)
     5.9      case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => new Color(255, 165, 0)
    5.10      case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => new Color(255, 106, 106)
    5.11    }
    5.12  
    5.13 +  val box_markup: PartialFunction[Text.Info[Any], Color] =
    5.14 +  {
    5.15 +    case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => new Color(192, 192, 192)
    5.16 +  }
    5.17 +
    5.18  
    5.19    /* document view of text area */
    5.20  
    5.21 @@ -245,6 +250,17 @@
    5.22                  }
    5.23                }
    5.24  
    5.25 +              // boxed text
    5.26 +              for {
    5.27 +                Text.Info(range, color) <-
    5.28 +                  snapshot.select_markup(line_range)(Document_View.box_markup)(null)
    5.29 +                if color != null
    5.30 +                r <- Isabelle.gfx_range(text_area, range)
    5.31 +              } {
    5.32 +                gfx.setColor(color)
    5.33 +                gfx.drawRect(r.x + 1, y + i * line_height + 1, r.length - 2, line_height - 3)
    5.34 +              }
    5.35 +
    5.36                // squiggly underline
    5.37                for {
    5.38                  Text.Info(range, color) <-