Syntax.read_asts error: report token ranges within message -- no side-effect here;
--- 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 *)
--- a/src/Pure/Syntax/syntax.ML Fri Sep 17 20:56:32 2010 +0200
+++ b/src/Pure/Syntax/syntax.ML Fri Sep 17 21:04:56 2010 +0200
@@ -710,7 +710,9 @@
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)
- handle ERROR msg => (List.app (Lexicon.report_token_range ctxt) toks; error msg);
+ handle ERROR msg =>
+ error (msg ^
+ implode (map (Markup.markup Markup.report o Lexicon.reported_token_range ctxt) toks));
val len = length pts;
val limit = Config.get ctxt ambiguity_limit;