bulk reports for improved message throughput;
authorwenzelm
Tue Sep 06 20:55:18 2011 +0200 (2011-09-06)
changeset 4473703a5ba7213cf
parent 44736 c2a3f1c84179
child 44758 deb929f002b8
bulk reports for improved message throughput;
src/Pure/ML/ml_compiler_polyml-5.3.ML
     1.1 --- a/src/Pure/ML/ml_compiler_polyml-5.3.ML	Tue Sep 06 20:37:07 2011 +0200
     1.2 +++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML	Tue Sep 06 20:55:18 2011 +0200
     1.3 @@ -34,31 +34,31 @@
     1.4  
     1.5  fun report_parse_tree depth space =
     1.6    let
     1.7 -    val report_text =
     1.8 +    val reported_text =
     1.9        (case Context.thread_data () of
    1.10 -        SOME (Context.Proof ctxt) => Context_Position.report_text ctxt
    1.11 -      | _ => Position.report_text);
    1.12 +        SOME (Context.Proof ctxt) => Context_Position.reported_text ctxt
    1.13 +      | _ => Position.reported_text);
    1.14  
    1.15 -    fun report_entity kind loc decl =
    1.16 -      report_text (position_of loc)
    1.17 +    fun reported_entity kind loc decl =
    1.18 +      reported_text (position_of loc)
    1.19          (Markup.entityN, (Markup.kindN, kind) :: Position.def_properties_of (position_of decl)) "";
    1.20  
    1.21 -    fun report loc (PolyML.PTtype types) =
    1.22 -          cons (fn () =>
    1.23 -            PolyML.NameSpace.displayTypeExpression (types, depth, space)
    1.24 -            |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
    1.25 -            |> report_text (position_of loc) Markup.ML_typing)
    1.26 -      | report loc (PolyML.PTdeclaredAt decl) =
    1.27 -          cons (fn () => report_entity Markup.ML_defN loc decl)
    1.28 -      | report loc (PolyML.PTopenedAt decl) =
    1.29 -          cons (fn () => report_entity Markup.ML_openN loc decl)
    1.30 -      | report loc (PolyML.PTstructureAt decl) =
    1.31 -          cons (fn () => report_entity Markup.ML_structN loc decl)
    1.32 -      | report _ (PolyML.PTnextSibling tree) = report_tree (tree ())
    1.33 -      | report _ (PolyML.PTfirstChild tree) = report_tree (tree ())
    1.34 -      | report _ _ = I
    1.35 -    and report_tree (loc, props) = fold (report loc) props;
    1.36 -  in fn tree => List.app (fn e => e ()) (report_tree tree []) end;
    1.37 +    fun reported loc (PolyML.PTtype types) =
    1.38 +          cons
    1.39 +            (PolyML.NameSpace.displayTypeExpression (types, depth, space)
    1.40 +              |> pretty_ml |> Pretty.from_ML |> Pretty.string_of
    1.41 +              |> reported_text (position_of loc) Markup.ML_typing)
    1.42 +      | reported loc (PolyML.PTdeclaredAt decl) =
    1.43 +          cons (reported_entity Markup.ML_defN loc decl)
    1.44 +      | reported loc (PolyML.PTopenedAt decl) =
    1.45 +          cons (reported_entity Markup.ML_openN loc decl)
    1.46 +      | reported loc (PolyML.PTstructureAt decl) =
    1.47 +          cons (reported_entity Markup.ML_structN loc decl)
    1.48 +      | reported _ (PolyML.PTnextSibling tree) = reported_tree (tree ())
    1.49 +      | reported _ (PolyML.PTfirstChild tree) = reported_tree (tree ())
    1.50 +      | reported _ _ = I
    1.51 +    and reported_tree (loc, props) = fold (reported loc) props;
    1.52 +  in fn tree => Output.report (implode (reported_tree tree [])) end;
    1.53  
    1.54  
    1.55  (* eval ML source tokens *)