bulk reports for improved message throughput;
authorwenzelm
Tue Sep 06 20:37:07 2011 +0200 (2011-09-06)
changeset 44736c2a3f1c84179
parent 44735 66862d02678c
child 44737 03a5ba7213cf
bulk reports for improved message throughput;
src/Pure/General/antiquote.ML
src/Pure/General/position.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/ML/ml_lex.ML
src/Pure/Syntax/lexicon.ML
src/Pure/Syntax/syntax_phases.ML
src/Pure/Thy/thy_syntax.ML
src/Pure/context_position.ML
     1.1 --- a/src/Pure/General/antiquote.ML	Tue Sep 06 19:48:57 2011 +0200
     1.2 +++ b/src/Pure/General/antiquote.ML	Tue Sep 06 20:37:07 2011 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4      Open of Position.T |
     1.5      Close of Position.T
     1.6    val is_text: 'a antiquote -> bool
     1.7 -  val report: ('a -> unit) -> 'a antiquote -> unit
     1.8 +  val reports_of: ('a -> Position.report list) -> 'a antiquote list -> Position.report list
     1.9    val check_nesting: 'a antiquote list -> unit
    1.10    val scan_antiq: Symbol_Pos.T list -> (Symbol_Pos.T list * Position.range) * Symbol_Pos.T list
    1.11    val scan: Symbol_Pos.T list -> 'a antiquote * Symbol_Pos.T list
    1.12 @@ -35,14 +35,14 @@
    1.13    | is_text _ = false;
    1.14  
    1.15  
    1.16 -(* report *)
    1.17 -
    1.18 -fun report_antiq pos = Position.report pos Markup.antiq;
    1.19 +(* reports *)
    1.20  
    1.21 -fun report report_text (Text x) = report_text x
    1.22 -  | report _ (Antiq (_, (pos, _))) = report_antiq pos
    1.23 -  | report _ (Open pos) = report_antiq pos
    1.24 -  | report _ (Close pos) = report_antiq pos;
    1.25 +fun reports_of text =
    1.26 +  maps
    1.27 +    (fn Text x => text x
    1.28 +      | Antiq (_, (pos, _)) => [(pos, Markup.antiq)]
    1.29 +      | Open pos => [(pos, Markup.antiq)]
    1.30 +      | Close pos => [(pos, Markup.antiq)]);
    1.31  
    1.32  
    1.33  (* check_nesting *)
    1.34 @@ -97,7 +97,7 @@
    1.35  
    1.36  fun read (syms, pos) =
    1.37    (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_text) syms of
    1.38 -    SOME xs => (List.app (report (K ())) xs; check_nesting xs; xs)
    1.39 +    SOME xs => (Position.reports (reports_of (K []) xs); check_nesting xs; xs)
    1.40    | NONE => error ("Malformed quotation/antiquotation source" ^ Position.str_of pos));
    1.41  
    1.42  end;
     2.1 --- a/src/Pure/General/position.ML	Tue Sep 06 19:48:57 2011 +0200
     2.2 +++ b/src/Pure/General/position.ML	Tue Sep 06 20:37:07 2011 +0200
     2.3 @@ -35,8 +35,9 @@
     2.4    val reported_text: T -> Markup.T -> string -> string
     2.5    val report_text: T -> Markup.T -> string -> unit
     2.6    val report: T -> Markup.T -> unit
     2.7 -  type reports = (T * Markup.T) list
     2.8 -  val store_reports: reports Unsynchronized.ref -> T list -> ('a -> Markup.T list) -> 'a -> unit
     2.9 +  type report = T * Markup.T
    2.10 +  val reports: report list -> unit
    2.11 +  val store_reports: report list Unsynchronized.ref -> T list -> ('a -> Markup.T list) -> 'a -> unit
    2.12    val str_of: T -> string
    2.13    type range = T * T
    2.14    val no_range: range
    2.15 @@ -154,10 +155,14 @@
    2.16  fun report_text pos markup txt = Output.report (reported_text pos markup txt);
    2.17  fun report pos markup = report_text pos markup "";
    2.18  
    2.19 -type reports = (T * Markup.T) list;
    2.20 +type report = T * Markup.T;
    2.21 +
    2.22 +val reports =
    2.23 +  map (fn (pos, m) => if is_reported pos then Markup.markup_only (markup pos m) else "")
    2.24 +  #> implode #> Output.report;
    2.25  
    2.26  fun store_reports _ [] _ _ = ()
    2.27 -  | store_reports (r: reports Unsynchronized.ref) ps markup x =
    2.28 +  | store_reports (r: report list Unsynchronized.ref) ps markup x =
    2.29        let val ms = markup x
    2.30        in Unsynchronized.change r (fold (fn p => fold (fn m => cons (p, m)) ms) ps) end;
    2.31  
     3.1 --- a/src/Pure/Isar/outer_syntax.ML	Tue Sep 06 19:48:57 2011 +0200
     3.2 +++ b/src/Pure/Isar/outer_syntax.ML	Tue Sep 06 20:37:07 2011 +0200
     3.3 @@ -258,7 +258,7 @@
     3.4    let
     3.5      val commands = lookup_commands outer_syntax;
     3.6      val range_pos = Position.set_range (Token.range toks);
     3.7 -    val _ = List.app Thy_Syntax.report_token toks;
     3.8 +    val _ = Position.reports (maps Thy_Syntax.reports_of_token toks);
     3.9    in
    3.10      (case Source.exhaust (toplevel_source false NONE (K commands) (Source.of_list toks)) of
    3.11        [tr] =>
     4.1 --- a/src/Pure/ML/ml_lex.ML	Tue Sep 06 19:48:57 2011 +0200
     4.2 +++ b/src/Pure/ML/ml_lex.ML	Tue Sep 06 20:37:07 2011 +0200
     4.3 @@ -20,7 +20,6 @@
     4.4    val content_of: token -> string
     4.5    val check_content_of: token -> string
     4.6    val flatten: token list -> string
     4.7 -  val report_token: token -> unit
     4.8    val keywords: string list
     4.9    val source: (Symbol.symbol, 'a) Source.source ->
    4.10      (token, (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source)
    4.11 @@ -126,7 +125,7 @@
    4.12  
    4.13  in
    4.14  
    4.15 -fun report_token (Token ((pos, _), (kind, x))) = Position.report pos (token_markup kind x);
    4.16 +fun report_of_token (Token ((pos, _), (kind, x))) = (pos, token_markup kind x);
    4.17  
    4.18  end;
    4.19  
    4.20 @@ -293,7 +292,7 @@
    4.21          |> Source.source Symbol_Pos.stopper (Scan.bulk (!!! "bad input" scan_antiq))
    4.22            (SOME (false, fn msg => recover msg >> map Antiquote.Text))
    4.23          |> Source.exhaust
    4.24 -        |> tap (List.app (Antiquote.report report_token))
    4.25 +        |> tap (Position.reports o Antiquote.reports_of (single o report_of_token))
    4.26          |> tap Antiquote.check_nesting
    4.27          |> tap (List.app (fn Antiquote.Text tok => (check_content_of tok; warn tok) | _ => ())))
    4.28        handle ERROR msg =>
     5.1 --- a/src/Pure/Syntax/lexicon.ML	Tue Sep 06 19:48:57 2011 +0200
     5.2 +++ b/src/Pure/Syntax/lexicon.ML	Tue Sep 06 20:37:07 2011 +0200
     5.3 @@ -44,7 +44,7 @@
     5.4    val tvarT: typ
     5.5    val terminals: string list
     5.6    val is_terminal: string -> bool
     5.7 -  val report_token: Proof.context -> token -> unit
     5.8 +  val report_of_token: token -> Position.report
     5.9    val reported_token_range: Proof.context -> token -> string
    5.10    val matching_tokens: token * token -> bool
    5.11    val valued_token: token -> bool
    5.12 @@ -203,11 +203,11 @@
    5.13    | Comment     => Markup.inner_comment
    5.14    | EOF         => Markup.empty;
    5.15  
    5.16 -fun report_token ctxt (Token (kind, s, (pos, _))) =
    5.17 +fun report_of_token (Token (kind, s, (pos, _))) =
    5.18    let val markup =
    5.19      if kind = Literal andalso not (is_ascii_identifier s) then Markup.delimiter
    5.20      else token_kind_markup kind
    5.21 -  in Context_Position.report ctxt pos markup end;
    5.22 +  in (pos, markup) end;
    5.23  
    5.24  fun reported_token_range ctxt tok =
    5.25    if is_proper tok
     6.1 --- a/src/Pure/Syntax/syntax_phases.ML	Tue Sep 06 19:48:57 2011 +0200
     6.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Tue Sep 06 20:37:07 2011 +0200
     6.3 @@ -10,7 +10,7 @@
     6.4    val term_sorts: term -> (indexname * sort) list
     6.5    val typ_of_term: (indexname -> sort) -> term -> typ
     6.6    val decode_term: Proof.context ->
     6.7 -    Position.reports * term Exn.result -> Position.reports * term Exn.result
     6.8 +    Position.report list * term Exn.result -> Position.report list * term Exn.result
     6.9    val parse_ast_pattern: Proof.context -> string * string -> Ast.ast
    6.10    val term_of_typ: Proof.context -> typ -> term
    6.11  end
    6.12 @@ -126,7 +126,7 @@
    6.13  
    6.14  fun parsetree_to_ast ctxt constrain_pos trf parsetree =
    6.15    let
    6.16 -    val reports = Unsynchronized.ref ([]: Position.reports);
    6.17 +    val reports = Unsynchronized.ref ([]: Position.report list);
    6.18      fun report pos = Position.store_reports reports [pos];
    6.19  
    6.20      fun trans a args =
    6.21 @@ -196,7 +196,7 @@
    6.22  
    6.23  (* decode_term -- transform parse tree into raw term *)
    6.24  
    6.25 -fun decode_term _ (result as (_: Position.reports, Exn.Exn _)) = result
    6.26 +fun decode_term _ (result as (_: Position.report list, Exn.Exn _)) = result
    6.27    | decode_term ctxt (reports0, Exn.Res tm) =
    6.28        let
    6.29          fun get_const a =
    6.30 @@ -262,12 +262,10 @@
    6.31  fun proper_results results = map_filter (fn (y, Exn.Res x) => SOME (y, x) | _ => NONE) results;
    6.32  fun failed_results results = map_filter (fn (y, Exn.Exn e) => SOME (y, e) | _ => NONE) results;
    6.33  
    6.34 -fun report ctxt = List.app (fn (pos, m) => Context_Position.report ctxt pos m);
    6.35 -
    6.36  fun report_result ctxt pos results =
    6.37    (case (proper_results results, failed_results results) of
    6.38 -    ([], (reports, exn) :: _) => (report ctxt reports; reraise exn)
    6.39 -  | ([(reports, x)], _) => (report ctxt reports; x)
    6.40 +    ([], (reports, exn) :: _) => (Context_Position.reports ctxt reports; reraise exn)
    6.41 +  | ([(reports, x)], _) => (Context_Position.reports ctxt reports; x)
    6.42    | _ => error (ambiguity_msg pos));
    6.43  
    6.44  
    6.45 @@ -279,7 +277,7 @@
    6.46      val ast_tr = Syntax.parse_ast_translation syn;
    6.47  
    6.48      val toks = Syntax.tokenize syn raw syms;
    6.49 -    val _ = List.app (Lexicon.report_token ctxt) toks;
    6.50 +    val _ = Context_Position.reports ctxt (map Lexicon.report_of_token toks);
    6.51  
    6.52      val pts = Syntax.parse ctxt syn root (filter Lexicon.is_proper toks)
    6.53        handle ERROR msg =>
     7.1 --- a/src/Pure/Thy/thy_syntax.ML	Tue Sep 06 19:48:57 2011 +0200
     7.2 +++ b/src/Pure/Thy/thy_syntax.ML	Tue Sep 06 20:37:07 2011 +0200
     7.3 @@ -11,7 +11,7 @@
     7.4        Source.source) Source.source) Source.source) Source.source
     7.5    val parse_tokens: Scan.lexicon * Scan.lexicon -> Position.T -> string -> Token.T list
     7.6    val present_token: Token.T -> Output.output
     7.7 -  val report_token: Token.T -> unit
     7.8 +  val reports_of_token: Token.T -> Position.report list
     7.9    datatype span_kind = Command of string | Ignored | Malformed
    7.10    type span
    7.11    val span_kind: span -> span_kind
    7.12 @@ -74,17 +74,17 @@
    7.13          else I;
    7.14      in props (token_kind_markup kind) end;
    7.15  
    7.16 -fun report_symbol (sym, pos) =
    7.17 -  if Symbol.is_malformed sym then Position.report pos Markup.malformed else ();
    7.18 +fun reports_of_symbol (sym, pos) =
    7.19 +  if Symbol.is_malformed sym then [(pos, Markup.malformed)] else [];
    7.20  
    7.21  in
    7.22  
    7.23  fun present_token tok =
    7.24    Markup.enclose (token_markup tok) (Output.output (Token.unparse tok));
    7.25  
    7.26 -fun report_token tok =
    7.27 - (Position.report (Token.position_of tok) (token_markup tok);
    7.28 -  List.app report_symbol (Symbol_Pos.explode (Token.source_position_of tok)));
    7.29 +fun reports_of_token tok =
    7.30 +  (Token.position_of tok, token_markup tok) ::
    7.31 +    maps reports_of_symbol (Symbol_Pos.explode (Token.source_position_of tok));
    7.32  
    7.33  end;
    7.34  
     8.1 --- a/src/Pure/context_position.ML	Tue Sep 06 19:48:57 2011 +0200
     8.2 +++ b/src/Pure/context_position.ML	Tue Sep 06 20:37:07 2011 +0200
     8.3 @@ -14,6 +14,7 @@
     8.4    val reported_text: Proof.context -> Position.T -> Markup.T -> string -> string
     8.5    val report_text: Proof.context -> Position.T -> Markup.T -> string -> unit
     8.6    val report: Proof.context -> Position.T -> Markup.T -> unit
     8.7 +  val reports: Proof.context -> Position.report list -> unit
     8.8  end;
     8.9  
    8.10  structure Context_Position: CONTEXT_POSITION =
    8.11 @@ -35,4 +36,6 @@
    8.12  fun report_text ctxt pos markup txt = Output.report (reported_text ctxt pos markup txt);
    8.13  fun report ctxt pos markup = report_text ctxt pos markup "";
    8.14  
    8.15 +fun reports ctxt reps = if is_visible ctxt then Position.reports reps else ();
    8.16 +
    8.17  end;