X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fcommon%2Foutput.ml;h=492b6d2c935d1a9ca7e99fbc1e913db695d11649;hb=2f19651bcec24abfb1bf15ff7e1387daad1f6638;hp=d84012c2f1d706876fbcf8c8e1a6e63be3f0eb6d;hpb=1be981691870cca039b1af1fb954491c2020d483;p=helm.git

diff --git a/helm/software/helena/src/common/output.ml b/helm/software/helena/src/common/output.ml
index d84012c2f..492b6d2c9 100644
--- a/helm/software/helena/src/common/output.ml
+++ b/helm/software/helena/src/common/output.ml
@@ -14,6 +14,8 @@ module KP = Printf
 module L  = Log
 module G  = Options
 
+IFDEF SUMMARY THEN
+
 type reductions = {
    beta   : int;
    zeta   : int;
@@ -43,11 +45,15 @@ let add
    ?(beta=0) ?(theta=0) ?(epsilon=0) ?(ldelta=0) ?(gdelta=0) ?(zeta=0) 
    ?(upsilon=0) ?(lrt=0) ?(grt=0) ?(e=0) ?(x=0) ()
 =
- if beta > 0 then L.warn level (KP.sprintf "BETA %u" beta);
- if ldelta > 0 then L.warn level (KP.sprintf "EXP %u" ldelta);
- if gdelta > 0 then L.warn level (KP.sprintf "EXP %u" gdelta);
- if lrt > 0 then L.warn level (KP.sprintf "EXP %u" lrt);
- if grt > 0 then L.warn level (KP.sprintf "EXP %u" grt); 
+(*
+   if !G.ct >= level then begin
+      if beta > 0 then L.warn level (KP.sprintf "BETA %u" beta);
+      if ldelta > 0 then L.warn level (KP.sprintf "EXP %u" ldelta);
+      if gdelta > 0 then L.warn level (KP.sprintf "EXP %u" gdelta);
+      if lrt > 0 then L.warn level (KP.sprintf "EXP %u" lrt);
+      if grt > 0 then L.warn level (KP.sprintf "EXP %u" grt); 
+   end;
+*)
 reductions := {
    beta = !reductions.beta + beta;
    zeta = !reductions.zeta + zeta;
@@ -83,5 +89,9 @@ let print_reductions () =
    L.warn level (KP.sprintf "      Local:                %7u" r.lrt);
    L.warn level (KP.sprintf "      Global:               %7u" r.grt);
    L.warn level (KP.sprintf "    Cast typing:            %7u" r.e);
-   L.warn level (KP.sprintf "    Binder typing:          %7u" r.x);  
+   L.warn level (KP.sprintf "    Binder typing:          %7u" r.x);
+IFDEF TYPE THEN
    L.warn level (KP.sprintf "Relocated nodes (icm):      %7u" !G.icm)
+ELSE () END
+
+END