]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/helena/src/automath/autOutput.ml
last commit for helena 0.8.2
[helm.git] / helm / software / helena / src / automath / autOutput.ml
index 028fdd23cb98444404454b385cec2c2cc08b4008..a1f5ae18c56e8c1fa97a2885ad9dbc3e144ece78 100644 (file)
@@ -9,7 +9,7 @@
      \ /   This software is distributed as is, NO WARRANTY.              
       V_______________________________________________________________ *)
 
-module  = Printf
+module KP = Printf
 
 module C  = Cps
 module L  = Log
@@ -73,31 +73,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 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 ()
 
 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