src/HOL/Tools/ATP/watcher.ML
changeset 17488 67376a311a2b
parent 17484 f6a225f97f0a
child 17502 8836793df947
     1.1 --- a/src/HOL/Tools/ATP/watcher.ML	Mon Sep 19 16:42:11 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Mon Sep 19 18:30:22 2005 +0200
     1.3 @@ -44,6 +44,7 @@
     1.4  (**********************************************************)
     1.5  
     1.6  val killWatcher : Posix.Process.pid -> unit
     1.7 +val killWatcher' : int -> unit
     1.8  
     1.9  end
    1.10  
    1.11 @@ -52,7 +53,7 @@
    1.12  structure Watcher: WATCHER =
    1.13  struct
    1.14  
    1.15 -open ReconPrelim Recon_Transfer
    1.16 +open Recon_Transfer
    1.17  
    1.18  val goals_being_watched = ref 0;
    1.19  
    1.20 @@ -401,8 +402,8 @@
    1.21  		   let val _ = File.append (File.tmp_path (Path.basic "child_check")) 
    1.22  			         "\nInput available from childIncoming" 
    1.23  		       val childDone = (case prover of
    1.24 -			   "vampire" => AtpCommunication.checkVampProofFound(childInput, toParentStr, parentID,goalstring, childCmd, thm, sg_num,clause_arr)  
    1.25 -			    | "E" => AtpCommunication.checkEProofFound(childInput, toParentStr, parentID,goalstring, childCmd, thm, sg_num,clause_arr)             
    1.26 +			   "vampire" => AtpCommunication.checkVampProofFound(childInput, toParentStr, parentID,goalstring, childCmd, clause_arr)  
    1.27 +			    | "E" => AtpCommunication.checkEProofFound(childInput, toParentStr, parentID,goalstring, childCmd, clause_arr)             
    1.28  			  |"spass" => AtpCommunication.checkSpassProofFound(childInput, toParentStr, parentID,goalstring, childCmd, thm, sg_num,clause_arr)  )
    1.29  		    in
    1.30  		     if childDone
    1.31 @@ -604,6 +605,8 @@
    1.32  
    1.33  fun killWatcher pid = Posix.Process.kill(Posix.Process.K_PROC pid, Posix.Signal.kill);
    1.34  
    1.35 +val killWatcher' = killWatcher o ResLib.pidOfInt;
    1.36 +
    1.37  fun reapWatcher(pid, instr, outstr) =
    1.38    (TextIO.closeIn instr; TextIO.closeOut outstr;
    1.39     Posix.Process.waitpid(Posix.Process.W_CHILD pid, []); ())