From: denes <??>
Date: Mon, 20 Jul 2009 17:58:07 +0000 (+0000)
Subject: Fixed multiple printing
X-Git-Tag: make_still_working~3650
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3f113993199aef5eb7f32773b637bf1716403403;p=helm.git

Fixed multiple printing
---

diff --git a/helm/software/components/binaries/matitaprover/matitaprover.ml b/helm/software/components/binaries/matitaprover/matitaprover.ml
index 7f9046eb3..df6abfa92 100644
--- a/helm/software/components/binaries/matitaprover/matitaprover.ml
+++ b/helm/software/components/binaries/matitaprover/matitaprover.ml
@@ -122,13 +122,13 @@ let report_error s =  prerr_endline (string_of_int (Unix.getpid())^": "^s);;
 
 module Main(P : Paramod.Paramod with type t = leaf) = struct
 
- let run ~useage stats goal hypotheses pp_unit_clause name = 
+ let run ~useage ~printmsg stats goal hypotheses pp_unit_clause name = 
    let bag = Terms.empty_bag, 0 in
    let bag, g_passives = P.mk_goal bag goal in
    let bag, passives = 
      HExtlib.list_mapi_acc (fun x _ b -> P.mk_passive b x) bag hypotheses 
    in
-   start_msg stats passives g_passives pp_unit_clause name;
+   if printmsg then start_msg stats passives g_passives pp_unit_clause name;
    match
      P.paramod ~useage
       ~max_steps:max_int bag ~g_passives:[g_passives] ~passives 
@@ -181,7 +181,7 @@ end
      data
  ;;
 
-let worker order ~useage goal hypotheses =
+let worker order ~useage ~printmsg goal hypotheses =
    let stats = compute_stats goal hypotheses in
    let module C = 
      struct
@@ -212,15 +212,15 @@ let worker order ~useage goal hypotheses =
    | `NRKBO ->
        let module O = Orderings.NRKBO(B) in
        let module Main = Main(Paramod.Paramod(O)) in
-       Main.run ~useage stats goal hypotheses Pp.pp_unit_clause O.name
+       Main.run ~useage ~printmsg stats goal hypotheses Pp.pp_unit_clause O.name
    | `KBO ->
        let module O = Orderings.KBO(B) in
        let module Main = Main(Paramod.Paramod(O)) in
-       Main.run ~useage stats goal hypotheses Pp.pp_unit_clause O.name
+       Main.run ~useage ~printmsg stats goal hypotheses Pp.pp_unit_clause O.name
    | `LPO ->
        let module O = Orderings.LPO(B) in
        let module Main = Main(Paramod.Paramod(O)) in
-       Main.run ~useage stats goal hypotheses Pp.pp_unit_clause O.name
+       Main.run ~useage ~printmsg stats goal hypotheses Pp.pp_unit_clause O.name
 ;;
 
 let print_status p = 
@@ -285,13 +285,13 @@ usage: matitaprover [options] problemfile";
          let pid = Unix.fork () in 
          if pid = 0 then (exit (f ())) else pid)
     [ 
-      (fun () -> worker `NRKBO ~useage:true goal hypotheses)
+      (fun () -> worker `NRKBO ~useage:true ~printmsg:true goal hypotheses)
     ;
-      (fun () -> worker `KBO ~useage:true goal hypotheses)
+      (fun () -> worker `KBO ~useage:true ~printmsg:false goal hypotheses)
     ;
-      (fun () -> worker `LPO ~useage:true goal hypotheses)
+      (fun () -> worker `LPO ~useage:true ~printmsg:false goal hypotheses)
     ;
-      (fun () -> worker `NRKBO ~useage:false goal hypotheses)
+      (fun () -> worker `NRKBO ~useage:false ~printmsg:false goal hypotheses)
     ];
   let rec aux () =
     if List.length !childs = 0 then