src/Pure/Syntax/syntax_phases.ML

--- a/src/Pure/Syntax/syntax_phases.ML	Tue Sep 06 19:48:57 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Tue Sep 06 20:37:07 2011 +0200
@@ -10,7 +10,7 @@
   val term_sorts: term -> (indexname * sort) list
   val typ_of_term: (indexname -> sort) -> term -> typ
   val decode_term: Proof.context ->
-    Position.reports * term Exn.result -> Position.reports * term Exn.result
+    Position.report list * term Exn.result -> Position.report list * term Exn.result
   val parse_ast_pattern: Proof.context -> string * string -> Ast.ast
   val term_of_typ: Proof.context -> typ -> term
 end
@@ -126,7 +126,7 @@
 
 fun parsetree_to_ast ctxt constrain_pos trf parsetree =
   let
-    val reports = Unsynchronized.ref ([]: Position.reports);
+    val reports = Unsynchronized.ref ([]: Position.report list);
     fun report pos = Position.store_reports reports [pos];
 
     fun trans a args =
@@ -196,7 +196,7 @@
 
 (* decode_term -- transform parse tree into raw term *)
 
-fun decode_term _ (result as (_: Position.reports, Exn.Exn _)) = result
+fun decode_term _ (result as (_: Position.report list, Exn.Exn _)) = result
   | decode_term ctxt (reports0, Exn.Res tm) =
       let
         fun get_const a =
@@ -262,12 +262,10 @@
 fun proper_results results = map_filter (fn (y, Exn.Res x) => SOME (y, x) | _ => NONE) results;
 fun failed_results results = map_filter (fn (y, Exn.Exn e) => SOME (y, e) | _ => NONE) results;
 
-fun report ctxt = List.app (fn (pos, m) => Context_Position.report ctxt pos m);
-
 fun report_result ctxt pos results =
   (case (proper_results results, failed_results results) of
-    ([], (reports, exn) :: _) => (report ctxt reports; reraise exn)
-  | ([(reports, x)], _) => (report ctxt reports; x)
+    ([], (reports, exn) :: _) => (Context_Position.reports ctxt reports; reraise exn)
+  | ([(reports, x)], _) => (Context_Position.reports ctxt reports; x)
   | _ => error (ambiguity_msg pos));
 
 
@@ -279,7 +277,7 @@
     val ast_tr = Syntax.parse_ast_translation syn;
 
     val toks = Syntax.tokenize syn raw syms;
-    val _ = List.app (Lexicon.report_token ctxt) toks;
+    val _ = Context_Position.reports ctxt (map Lexicon.report_of_token toks);
 
     val pts = Syntax.parse ctxt syn root (filter Lexicon.is_proper toks)
       handle ERROR msg =>