--- a/src/Pure/Syntax/lexicon.ML Fri Sep 17 20:56:32 2010 +0200
+++ b/src/Pure/Syntax/lexicon.ML Fri Sep 17 21:04:56 2010 +0200
@@ -66,7 +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 reported_token_range: Proof.context -> token -> string
val matching_tokens: token * token -> bool
val valued_token: token -> bool
val predef_term: string -> token option
@@ -189,10 +189,10 @@
fun report_token ctxt (Token (kind, _, (pos, _))) =
Context_Position.report ctxt pos (token_kind_markup kind);
-fun report_token_range ctxt tok =
+fun reported_token_range ctxt tok =
if is_proper tok
- then Context_Position.report ctxt (pos_of_token tok) Markup.token_range
- else ();
+ then Context_Position.reported_text ctxt (pos_of_token tok) Markup.token_range ""
+ else "";
(* matching_tokens *)