diff -r 803431dcc7fb -r e3ac771235f7 src/Pure/Syntax/lexicon.ML
--- 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 *)