X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fmatitaprover.ml;fp=helm%2Fsoftware%2Fmatita%2Fmatitaprover.ml;h=d085b350c8db1b4d0df21f1d9d9e72596181ed71;hb=4ab3123d6a8e5080009d7b471b0cefd05f4817ed;hp=b3115ec26e6feefff346bfba3ebb9f36b8053035;hpb=0a50912f2577243a1f9e4068b02877b8e61181c9;p=helm.git

diff --git a/helm/software/matita/matitaprover.ml b/helm/software/matita/matitaprover.ml
index b3115ec26..d085b350c 100644
--- a/helm/software/matita/matitaprover.ml
+++ b/helm/software/matita/matitaprover.ml
@@ -74,9 +74,9 @@ for @{ 'exists ${default
 "
 ;;
 
-let p_to_ma ~tptppath ~filename = 
+let p_to_ma ?timeout ~tptppath ~filename () = 
   let data = 
-     Tptp2grafite.tptp2grafite ~filename ~tptppath:tptppath
+     Tptp2grafite.tptp2grafite ?timeout ~filename ~tptppath:tptppath
      ~raw_preamble ()
   in
   data
@@ -85,9 +85,12 @@ let p_to_ma ~tptppath ~filename =
 let main () =
   MatitaInit.fill_registry ();
   let tptppath = ref "./" in
+  let timeout = ref 600 in
   MatitaInit.add_cmdline_spec
     ["-tptppath",Arg.String (fun s -> tptppath:= s),
-      "Where to find the Axioms/ and Problems/ directory"];
+       "Where to find the Axioms/ and Problems/ directory";
+     "-timeout", Arg.Int (fun x -> timeout := x),
+       "Timeout in seconds"];
   MatitaInit.parse_cmdline ();
   MatitaInit.load_configuration_file ();
   Helm_registry.set_bool "db.nodb" true;
@@ -99,7 +102,9 @@ let main () =
     | [file] -> file
     | _ -> prerr_endline "You must specify exactly one .p file."; exit 1
   in
-  let data = p_to_ma ~filename:inputfile ~tptppath:!tptppath in
+  let data = 
+    p_to_ma ~timeout:!timeout ~filename:inputfile ~tptppath:!tptppath ()
+  in
 (*   prerr_endline data; *)
   let is = Ulexing.from_utf8_string data in
   let gs = GrafiteSync.init () in