src/HOL/Tools/ATP/watcher.ML
changeset 15652 a9d65894962e
parent 15642 028059faa963
child 15658 2edb384bf61f
     1.1 --- a/src/HOL/Tools/ATP/watcher.ML	Sat Apr 02 00:33:51 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Mon Apr 04 18:39:45 2005 +0200
     1.3 @@ -19,11 +19,11 @@
     1.4  use "modUnix";*)
     1.5  (*use "/homes/clq20/Jia_Code/TransStartIsar";*)
     1.6  
     1.7 -use "~~/VampireCommunication";
     1.8 -use "~~/SpassCommunication";
     1.9 +use "~~/src/HOL/Tools/ATP/VampireCommunication.ML";
    1.10 +use "~~/src/HOL/Tools/ATP/SpassCommunication.ML";
    1.11  
    1.12  
    1.13 -use "~~/modUnix";
    1.14 +use "~~/src/HOL/Tools/ATP/modUnix.ML";
    1.15  
    1.16  
    1.17  structure Watcher: WATCHER =
    1.18 @@ -34,7 +34,6 @@
    1.19  
    1.20  val goals_being_watched = ref 0;
    1.21  
    1.22 -
    1.23  fun remove y [] = []
    1.24  |   remove y (x::xs) = (if y = x 
    1.25                         then 
    1.26 @@ -98,7 +97,7 @@
    1.27                                                       let 
    1.28                                                          val dfg_dir = File.tmp_path (Path.basic "dfg");
    1.29                                                          (* need to check here if the directory exists and, if not, create it*)
    1.30 -                                                         val  outfile = TextIO.openAppend(" /thmstring_in_watcher");                                                                                    
    1.31 +                                                         val  outfile = TextIO.openAppend("thmstring_in_watcher");                                                                                    
    1.32                                                           val _ = TextIO.output (outfile, (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^"\n"))
    1.33                                                           val _ =  TextIO.closeOut outfile
    1.34                                                           val dfg_create =if File.exists dfg_dir 
    1.35 @@ -386,7 +385,7 @@
    1.36                                                           (childProc::(checkChildren (otherChildren, toParentStr)))
    1.37                                                   end
    1.38                                                 else
    1.39 -                                                   let val  outfile = TextIO.openOut("child_incoming");  
    1.40 +                                                   let val  outfile = TextIO.openAppend("child_incoming");  
    1.41                                                  val _ = TextIO.output (outfile,"No child output " )
    1.42                                                  val _ =  TextIO.closeOut outfile
    1.43                                                   in