X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbin%2Frecomm%2Frecomm.ml;h=87caeb10b960a18857265629d23863866106b30b;hb=8fdf1af656038d0245eba64ff2531bbe94ce0e9e;hp=a2336ad9c058a0301a2a3e3d7483c828488ce415;hpb=baa54e5db0fb93c4242dd1b67a5018ca63206cf6;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/bin/recomm/recomm.ml b/matita/matita/contribs/lambdadelta/bin/recomm/recomm.ml index a2336ad9c..87caeb10b 100644 --- a/matita/matita/contribs/lambdadelta/bin/recomm/recomm.ml +++ b/matita/matita/contribs/lambdadelta/bin/recomm/recomm.ml @@ -5,14 +5,30 @@ module EO = RecommOutput module P1 = RecommPccFor module P2 = RecommPcsAnd +module P3 = RecommPcsPar module G = RecommGc let write = ref false +let force = ref false + +let subst = ref None + let chdir path = Sys.chdir path +let start_substs () = + subst := Some (open_out "subst.txt") + +let write_substs lint = function + | None -> () + | Some och -> EO.write_substs och lint + +let stop_substs = function + | None -> () + | Some och -> close_out och + let rec process path name = let file = Filename.concat path name in if Sys.is_directory file then begin @@ -23,7 +39,8 @@ let rec process path name = Printf.eprintf "processing: %S\n" file; let orig = EI.read_srcs file in let lint = EC.recomm_srcs orig in - if !write && lint <> orig then EO.write_srcs file lint + write_substs lint !subst; + if !force || (!write && lint <> orig) then EO.write_srcs file lint end else begin Printf.eprintf "skipping: %S\n" file end @@ -32,13 +49,16 @@ let msg_C = "