X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fautomath%2FautOutput.ml;h=f9272867c58158d385a94b68f74f9237e4d93d6c;hb=refs%2Fheads%2Fmatita-lablgtk3;hp=ddf2f30edaa122866fa98b9e65b5a4f01b524107;hpb=95872555aaa040a22ad2d93cb1278f79e20da70c;p=helm.git

diff --git a/helm/software/helena/src/automath/autOutput.ml b/helm/software/helena/src/automath/autOutput.ml
index ddf2f30ed..f9272867c 100644
--- a/helm/software/helena/src/automath/autOutput.ml
+++ b/helm/software/helena/src/automath/autOutput.ml
@@ -9,7 +9,8 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
-module P  = Printf
+module KP = Printf
+
 module C  = Cps
 module L  = Log
 module A  = Aut
@@ -29,11 +30,15 @@ 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
 }
 
+IFDEF SUMMARY THEN
+
 let rec count_term f c = function
    | A.Sort _         -> 
       f {c with sorts = succ c.sorts; xnodes = succ c.xnodes}
@@ -70,31 +75,37 @@ 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 (KP.sprintf "Automath representation summary");
+   L.warn level (KP.sprintf "  Total book entities:      %7u" entities);
+   L.warn level (KP.sprintf "    Section entities:       %7u" c.sections);
+   L.warn level (KP.sprintf "    Context entities:       %7u" c.contexts);
+   L.warn level (KP.sprintf "    Block entities:         %7u" c.blocks);
+   L.warn level (KP.sprintf "    Declaration entities:   %7u" c.decls);
+   L.warn level (KP.sprintf "    Definition entities:    %7u" c.defs);
+   L.warn level (KP.sprintf "  Total Parameter items:    %7u" c.pars);
+   L.warn level (KP.sprintf "    Application items:      %7u" c.pars);
+   L.warn level (KP.sprintf "  Total term items:         %7u" terms);
+   L.warn level (KP.sprintf "    Sort items:             %7u" c.sorts);
+   L.warn level (KP.sprintf "    Reference items:        %7u" c.grefs);
+   L.warn level (KP.sprintf "    Application items:      %7u" c.appls);
+   L.warn level (KP.sprintf "    Abstraction items:      %7u" c.absts);
+   L.warn level (KP.sprintf "  Global Int. Complexity:   unknown");
+   L.warn level (KP.sprintf "    + Abbreviation nodes:   %7u" c.xnodes);
    f ()
 
+IFDEF PREPROCESS THEN
+
 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 (KP.sprintf "Automath process summary");
+      L.warn level (KP.sprintf "  Implicit after opening:   %7u" iao);
+      L.warn level (KP.sprintf "  Implicit after reopening: %7u" iar);
+      L.warn level (KP.sprintf "  Implicit after closing:   %7u" iac);
+      L.warn level (KP.sprintf "  Implicit after global:    %7u" iag);
       f ()
    in
    AA.get_counters f c
+
+END
+
+END