src/HOL/Tools/ATP/watcher.ML
changeset 17150 ce2a1aeb42aa
parent 17121 4c225f640b89
child 17216 df66d8feec63
     1.1 --- a/src/HOL/Tools/ATP/watcher.ML	Fri Aug 26 10:01:06 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Fri Aug 26 19:36:07 2005 +0200
     1.3 @@ -274,7 +274,7 @@
     1.4      (*** hyps/local axioms just now                                                ***)
     1.5      val whole_prob_file = Unix.execute("/bin/cat", [clasimpfile,(*axfile, hypsfile,*)probfile,  ">", (File.platform_path wholefile)])
     1.6      (*** check if the directory exists and, if not, create it***)
     1.7 -    val _ = 
     1.8 +   (* val _ = 
     1.9  	if !SpassComm.spass
    1.10  	then 
    1.11  	    if File.exists dfg_dir then warning("dfg dir exists")
    1.12 @@ -292,7 +292,16 @@
    1.13  			    dfg_path^"/ax_prob"^"_"^(probID)^".dfg" 
    1.14  
    1.15  		    else
    1.16 -			    (File.platform_path wholefile)
    1.17 +			    (File.platform_path wholefile)*)
    1.18 +
    1.19 +    (* if using spass prob_n already contains whole DFG file, otherwise need to mash axioms*)
    1.20 +    (* from clasimpset onto problem file *)
    1.21 +    val newfile =   if !SpassComm.spass 
    1.22 +		    then 
    1.23 +			 probfile
    1.24 +                    else 
    1.25 +			(File.platform_path wholefile)
    1.26 +
    1.27      val _ =  File.append (File.tmp_path (Path.basic"thmstring_in_watcher"))
    1.28  	       (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^newfile^"\n")
    1.29    in
    1.30 @@ -516,10 +525,10 @@
    1.31                          val _ = File.append (File.tmp_path (Path.basic "child_command")) 
    1.32  			           (childCmd^"\n")
    1.33  			(* now get the number of the subgoal from the filename *)
    1.34 -			val sg_num = if (!SpassComm.spass )
    1.35 +			val sg_num = (*if (!SpassComm.spass )
    1.36  				     then 
    1.37  					int_of_string(ReconOrderClauses.get_nth 5 (rev(explode childCmd)))
    1.38 -				     else
    1.39 +				     else*)
    1.40  					int_of_string(hd (rev(explode childCmd)))
    1.41  
    1.42  			val childIncoming = pollChildInput childInput