we now do some static analysis on the Automath text to possibly clear some language...

[helm.git] / helm / software / lambda-delta / automath / autOutput.ml

diff --git a/helm/software/lambda-delta/automath/autOutput.ml b/helm/software/lambda-delta/automath/autOutput.ml
index ffbdfdb2096eeac175e3e86ee1af854c60fe100a..6ca42e6c640a165a65e2955a2421b7d6d7b07c8a 100644 (file)
--- a/helm/software/lambda-delta/automath/autOutput.ml
+++ b/helm/software/lambda-delta/automath/autOutput.ml
@@ -12,6 +12,7 @@
 module P = Printf
 module L = Log
 module A = Aut
+module R = AutProcess
 
 type counters = {
    sections: int;
@@ -85,3 +86,13 @@ let print_counters f c =
    L.warn (P.sprintf "    Global Int. Complexity:   unknown");
    L.warn (P.sprintf "      + Abbreviation nodes:   %7u" c.xnodes);
    f ()
+
+let print_process_counters f c =
+   let f iao iar iac =
+      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);
+      f ()
+   in
+   R.get_counters f c