bulk reports for improved message throughput;

--- a/src/Pure/General/antiquote.ML	Tue Sep 06 19:48:57 2011 +0200
+++ b/src/Pure/General/antiquote.ML	Tue Sep 06 20:37:07 2011 +0200
@@ -12,7 +12,7 @@
     Open of Position.T |
     Close of Position.T
   val is_text: 'a antiquote -> bool
-  val report: ('a -> unit) -> 'a antiquote -> unit
+  val reports_of: ('a -> Position.report list) -> 'a antiquote list -> Position.report list
   val check_nesting: 'a antiquote list -> unit
   val scan_antiq: Symbol_Pos.T list -> (Symbol_Pos.T list * Position.range) * Symbol_Pos.T list
   val scan: Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list
@@ -35,14 +35,14 @@
   | is_text _ = false;
 
 
-(* report *)
-
-fun report_antiq pos = Position.report pos Markup.antiq;
+(* reports *)
 
-fun report report_text (Text x) = report_text x
-  | report _ (Antiq (_, (pos, _))) = report_antiq pos
-  | report _ (Open pos) = report_antiq pos
-  | report _ (Close pos) = report_antiq pos;
+fun reports_of text =
+  maps
+    (fn Text x => text x
+      | Antiq (_, (pos, _)) => [(pos, Markup.antiq)]
+      | Open pos => [(pos, Markup.antiq)]
+      | Close pos => [(pos, Markup.antiq)]);
 
 
 (* check_nesting *)
@@ -97,7 +97,7 @@
 
 fun read (syms, pos) =
   (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_text) syms of
-    SOME xs => (List.app (report (K ())) xs; check_nesting xs; xs)
+    SOME xs => (Position.reports (reports_of (K []) xs); check_nesting xs; xs)
   | NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos));
 
 end;

--- a/src/Pure/General/position.ML	Tue Sep 06 19:48:57 2011 +0200
+++ b/src/Pure/General/position.ML	Tue Sep 06 20:37:07 2011 +0200
@@ -35,8 +35,9 @@
   val reported_text: T -> Markup.T -> string -> string
   val report_text: T -> Markup.T -> string -> unit
   val report: T -> Markup.T -> unit
-  type reports = (T * Markup.T) list
-  val store_reports: reports Unsynchronized.ref -> T list -> ('a -> Markup.T list) -> 'a -> unit
+  type report = T * Markup.T
+  val reports: report list -> unit
+  val store_reports: report list Unsynchronized.ref -> T list -> ('a -> Markup.T list) -> 'a -> unit
   val str_of: T -> string
   type range = T * T
   val no_range: range
@@ -154,10 +155,14 @@
 fun report_text pos markup txt = Output.report (reported_text pos markup txt);
 fun report pos markup = report_text pos markup "";
 
-type reports = (T * Markup.T) list;
+type report = T * Markup.T;
+
+val reports =
+  map (fn (pos, m) => if is_reported pos then Markup.markup_only (markup pos m) else "")
+  #> implode #> Output.report;
 
 fun store_reports _ [] _ _ = ()
-  | store_reports (r: reports Unsynchronized.ref) ps markup x =
+  | store_reports (r: report list Unsynchronized.ref) ps markup x =
       let val ms = markup x
       in Unsynchronized.change r (fold (fn p => fold (fn m => cons (p, m)) ms) ps) end;
 

--- a/src/Pure/Isar/outer_syntax.ML	Tue Sep 06 19:48:57 2011 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Tue Sep 06 20:37:07 2011 +0200
@@ -258,7 +258,7 @@
   let
     val commands = lookup_commands outer_syntax;
     val range_pos = Position.set_range (Token.range toks);
-    val _ = List.app Thy_Syntax.report_token toks;
+    val _ = Position.reports (maps Thy_Syntax.reports_of_token toks);
   in
     (case Source.exhaust (toplevel_source false NONE (K commands) (Source.of_list toks)) of
       [tr] =>

--- a/src/Pure/ML/ml_lex.ML	Tue Sep 06 19:48:57 2011 +0200
+++ b/src/Pure/ML/ml_lex.ML	Tue Sep 06 20:37:07 2011 +0200
@@ -20,7 +20,6 @@
   val content_of: token -> string
   val check_content_of: token -> string
   val flatten: token list -> string
-  val report_token: token -> unit
   val keywords: string list
   val source: (Symbol.symbol, 'a) Source.source ->
     (token, (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source)
@@ -126,7 +125,7 @@
 
 in
 
-fun report_token (Token ((pos, _), (kind, x))) = Position.report pos (token_markup kind x);
+fun report_of_token (Token ((pos, _), (kind, x))) = (pos, token_markup kind x);
 
 end;
 
@@ -293,7 +292,7 @@
         |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_antiq))
           (SOME (false, fn msg => recover msg >> map Antiquote.Text))
         |> Source.exhaust
-        |> tap (List.app (Antiquote.report report_token))
+        |> tap (Position.reports o Antiquote.reports_of (single o report_of_token))
         |> tap Antiquote.check_nesting
         |> tap (List.app (fn Antiquote.Text tok => (check_content_of tok; warn tok) | _ => ())))
       handle ERROR msg =>

--- a/src/Pure/Syntax/lexicon.ML	Tue Sep 06 19:48:57 2011 +0200
+++ b/src/Pure/Syntax/lexicon.ML	Tue Sep 06 20:37:07 2011 +0200
@@ -44,7 +44,7 @@
   val tvarT: typ
   val terminals: string list
   val is_terminal: string -> bool
-  val report_token: Proof.context -> token -> unit
+  val report_of_token: token -> Position.report
   val reported_token_range: Proof.context -> token -> string
   val matching_tokens: token * token -> bool
   val valued_token: token -> bool
@@ -203,11 +203,11 @@
   | Comment     => Markup.inner_comment
   | EOF         => Markup.empty;
 
-fun report_token ctxt (Token (kind, s, (pos, _))) =
+fun report_of_token (Token (kind, s, (pos, _))) =
   let val markup =
     if kind = Literal andalso not (is_ascii_identifier s) then Markup.delimiter
     else token_kind_markup kind
-  in Context_Position.report ctxt pos markup end;
+  in (pos, markup) end;
 
 fun reported_token_range ctxt tok =
   if is_proper tok

--- 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 =>

--- a/src/Pure/Thy/thy_syntax.ML	Tue Sep 06 19:48:57 2011 +0200
+++ b/src/Pure/Thy/thy_syntax.ML	Tue Sep 06 20:37:07 2011 +0200
@@ -11,7 +11,7 @@
       Source.source) Source.source) Source.source) Source.source
   val parse_tokens: Scan.lexicon * Scan.lexicon -> Position.T -> string -> Token.T list
   val present_token: Token.T -> Output.output
-  val report_token: Token.T -> unit
+  val reports_of_token: Token.T -> Position.report list
   datatype span_kind = Command of string | Ignored | Malformed
   type span
   val span_kind: span -> span_kind
@@ -74,17 +74,17 @@
         else I;
     in props (token_kind_markup kind) end;
 
-fun report_symbol (sym, pos) =
-  if Symbol.is_malformed sym then Position.report pos Markup.malformed else ();
+fun reports_of_symbol (sym, pos) =
+  if Symbol.is_malformed sym then [(pos, Markup.malformed)] else [];
 
 in
 
 fun present_token tok =
   Markup.enclose (token_markup tok) (Output.output (Token.unparse tok));
 
-fun report_token tok =
- (Position.report (Token.position_of tok) (token_markup tok);
-  List.app report_symbol (Symbol_Pos.explode (Token.source_position_of tok)));
+fun reports_of_token tok =
+  (Token.position_of tok, token_markup tok) ::
+    maps reports_of_symbol (Symbol_Pos.explode (Token.source_position_of tok));
 
 end;
 

--- a/src/Pure/context_position.ML	Tue Sep 06 19:48:57 2011 +0200
+++ b/src/Pure/context_position.ML	Tue Sep 06 20:37:07 2011 +0200
@@ -14,6 +14,7 @@
   val reported_text: Proof.context -> Position.T -> Markup.T -> string -> string
   val report_text: Proof.context -> Position.T -> Markup.T -> string -> unit
   val report: Proof.context -> Position.T -> Markup.T -> unit
+  val reports: Proof.context -> Position.report list -> unit
 end;
 
 structure Context_Position: CONTEXT_POSITION =
@@ -35,4 +36,6 @@
 fun report_text ctxt pos markup txt = Output.report (reported_text ctxt pos markup txt);
 fun report ctxt pos markup = report_text ctxt pos markup "";
 
+fun reports ctxt reps = if is_visible ctxt then Position.reports reps else ();
+
 end;