# HG changeset patch
# User wenzelm
# Date 1284750296 -7200
# Node ID d9f5f01faa1b6ef7b70aa3d0468e0c2f3fa75a30
# Parent  cab2719398a75b3837731685c6ad520ef2ef3abb
Syntax.read_asts error: report token ranges within message -- no side-effect here;

diff -r cab2719398a7 -r d9f5f01faa1b src/Pure/Syntax/lexicon.ML
--- 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 *)
diff -r cab2719398a7 -r d9f5f01faa1b src/Pure/Syntax/syntax.ML
--- 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;