new message reporting system improves performance significatively

[helm.git] / helm / software / helena / src / automath / autOutput.ml

diff --git a/helm/software/helena/src/automath/autOutput.ml b/helm/software/helena/src/automath/autOutput.ml
index ddf2f30edaa122866fa98b9e65b5a4f01b524107..41424b4db50b6dd42fea808ff49f49431ab4706b 100644 (file)
--- a/helm/software/helena/src/automath/autOutput.ml
+++ b/helm/software/helena/src/automath/autOutput.ml
@@ -29,6 +29,8 @@ type counters = {
    xnodes:   int
 }
 
+let level = 2
+
 let initial_counters = {
    sections = 0; contexts = 0; blocks = 0; decls = 0; defs = 0;
    sorts = 0; grefs = 0; appls = 0; absts = 0; pars = 0; xnodes = 0
@@ -70,31 +72,31 @@ let count_command f c = function
 let print_counters f c =
    let terms = c.sorts + c.grefs + c.appls + c.absts in
    let entities = c.sections + c.contexts + c.blocks + c.decls + c.defs in
-   L.warn (P.sprintf "  Automath representation summary");
-   L.warn (P.sprintf "    Total book entities:      %7u" entities);
-   L.warn (P.sprintf "      Section entities:       %7u" c.sections);
-   L.warn (P.sprintf "      Context entities:       %7u" c.contexts);
-   L.warn (P.sprintf "      Block entities:         %7u" c.blocks);
-   L.warn (P.sprintf "      Declaration entities:   %7u" c.decls);
-   L.warn (P.sprintf "      Definition entities:    %7u" c.defs);
-   L.warn (P.sprintf "    Total Parameter items:    %7u" c.pars);
-   L.warn (P.sprintf "      Application items:      %7u" c.pars);
-   L.warn (P.sprintf "    Total term items:         %7u" terms);
-   L.warn (P.sprintf "      Sort items:             %7u" c.sorts);
-   L.warn (P.sprintf "      Reference items:        %7u" c.grefs);
-   L.warn (P.sprintf "      Application items:      %7u" c.appls);
-   L.warn (P.sprintf "      Abstraction items:      %7u" c.absts);
-   L.warn (P.sprintf "    Global Int. Complexity:   unknown");
-   L.warn (P.sprintf "      + Abbreviation nodes:   %7u" c.xnodes);
+   L.warn level (P.sprintf "Automath representation summary");
+   L.warn level (P.sprintf "  Total book entities:      %7u" entities);
+   L.warn level (P.sprintf "    Section entities:       %7u" c.sections);
+   L.warn level (P.sprintf "    Context entities:       %7u" c.contexts);
+   L.warn level (P.sprintf "    Block entities:         %7u" c.blocks);
+   L.warn level (P.sprintf "    Declaration entities:   %7u" c.decls);
+   L.warn level (P.sprintf "    Definition entities:    %7u" c.defs);
+   L.warn level (P.sprintf "  Total Parameter items:    %7u" c.pars);
+   L.warn level (P.sprintf "    Application items:      %7u" c.pars);
+   L.warn level (P.sprintf "  Total term items:         %7u" terms);
+   L.warn level (P.sprintf "    Sort items:             %7u" c.sorts);
+   L.warn level (P.sprintf "    Reference items:        %7u" c.grefs);
+   L.warn level (P.sprintf "    Application items:      %7u" c.appls);
+   L.warn level (P.sprintf "    Abstraction items:      %7u" c.absts);
+   L.warn level (P.sprintf "  Global Int. Complexity:   unknown");
+   L.warn level (P.sprintf "    + Abbreviation nodes:   %7u" c.xnodes);
    f ()
 
 let print_process_counters f c =
    let f iao iar iac iag =
-      L.warn (P.sprintf "  Automath process summary");
-      L.warn (P.sprintf "    Implicit after opening:   %7u" iao);
-      L.warn (P.sprintf "    Implicit after reopening: %7u" iar);
-      L.warn (P.sprintf "    Implicit after closing:   %7u" iac);
-      L.warn (P.sprintf "    Implicit after global:    %7u" iag);
+      L.warn level (P.sprintf "Automath process summary");
+      L.warn level (P.sprintf "  Implicit after opening:   %7u" iao);
+      L.warn level (P.sprintf "  Implicit after reopening: %7u" iar);
+      L.warn level (P.sprintf "  Implicit after closing:   %7u" iac);
+      L.warn level (P.sprintf "  Implicit after global:    %7u" iag);
       f ()
    in
    AA.get_counters f c