X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fautomath%2FautOutput.ml;h=f9272867c58158d385a94b68f74f9237e4d93d6c;hb=600fba840c748f67593838673a6eb40eab9b68e5;hp=028fdd23cb98444404454b385cec2c2cc08b4008;hpb=34e6104ef149e3776d0ab7f0930ae73f0e8de157;p=helm.git

diff --git a/helm/software/helena/src/automath/autOutput.ml b/helm/software/helena/src/automath/autOutput.ml
index 028fdd23c..f9272867c 100644
--- a/helm/software/helena/src/automath/autOutput.ml
+++ b/helm/software/helena/src/automath/autOutput.ml
@@ -9,7 +9,7 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
-module P  = Printf
+module KP = Printf
 
 module C  = Cps
 module L  = Log
@@ -37,6 +37,8 @@ let initial_counters = {
    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}
@@ -73,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 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);
+   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 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);
+      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