src/HOL/Tools/ATP/watcher.ML
changeset 16091 3683f0486a11
parent 16089 9169bdf930f8
child 16100 f80fc4bff933
     1.1 --- a/src/HOL/Tools/ATP/watcher.ML	Thu May 26 16:50:20 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Thu May 26 18:34:23 2005 +0200
     1.3 @@ -164,7 +164,7 @@
     1.4  			(thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^"\n"))
     1.5  	  val _ =  TextIO.closeOut outfile
     1.6  	 (*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***)
     1.7 -	 val probID = ReconOrderClauses.last(explode probfile)
     1.8 +	  val probID = ReconOrderClauses.last(explode probfile)
     1.9  	  val wholefile = File.tmp_path (Path.basic ("ax_prob_"^probID))
    1.10  	  (*** only include problem and clasimp for the moment, not sure how to refer to ***)
    1.11  	  (*** hyps/local axioms just now                                                ***)
    1.12 @@ -174,16 +174,16 @@
    1.13  			   else File.mkdir dfg_dir; 
    1.14  	  
    1.15  	  val dfg_path = File.sysify_path dfg_dir;
    1.16 +	  val tptp2x_args = ["-fdfg", "-d " ^ dfg_path, File.sysify_path wholefile]
    1.17  	  val exec_tptp2x = 
    1.18 -	        Unix.execute(getenv "TPTP2X_HOME" ^ "/tptp2X",  
    1.19 -	                     ["-fdfg", "-d " ^ dfg_path, File.sysify_path wholefile])
    1.20 + 	      Unix.execute(getenv "TPTP2X_HOME" ^ "/tptp2X", tptp2x_args)
    1.21  	(*val _ = Posix.Process.wait ()*)
    1.22  	(*val _ =Unix.reap exec_tptp2x*)
    1.23  	  val newfile = dfg_path^"/ax_prob"^"_"^(probID)^".dfg"
    1.24   
    1.25         in   
    1.26  	  goals_being_watched := (!goals_being_watched) + 1;
    1.27 -	  Posix.Process.sleep(Time.fromSeconds 1); 
    1.28 +	  Posix.Process.sleep(Time.fromSeconds 4); 
    1.29  	  (warning ("probfile is: "^probfile));
    1.30  	  (warning("dfg file is: "^newfile));
    1.31  	  (warning ("wholefile is: "^(File.sysify_path wholefile)));
    1.32 @@ -196,8 +196,8 @@
    1.33  	  if File.exists
    1.34  	        (Path.append dfg_dir (Path.basic ("ax_prob"^"_" ^ probID ^ ".dfg")))
    1.35  	  then callResProvers (toWatcherStr, args)
    1.36 -	  else error ("tptp2X failed: " ^ getenv "TPTP2X_HOME" ^ "/tptp2X" ^
    1.37 -	              " -fdfg " ^ File.sysify_path wholefile ^ " -d " ^ dfg_path)
    1.38 +	  else error ("tptp2X failed: " ^ getenv "TPTP2X_HOME" ^ "/tptp2X " ^
    1.39 +	              space_implode " " tptp2x_args)
    1.40        end
    1.41  (*
    1.42  fun callResProversStr (toWatcherStr,  []) =  "End of calls\n"