# HG changeset patch
# User paulson
# Date 1142009829 -3600
# Node ID 31c1143372247b5d5365631b1c3de919023ee7cc
# Parent  a2a4e6838bfcf543f16e475f401f3fd106bd6558
exporting reapAll and killChild

diff -r a2a4e6838bfc -r 31c114337224 src/HOL/Tools/ATP/watcher.ML
--- a/src/HOL/Tools/ATP/watcher.ML	Fri Mar 10 17:53:53 2006 +0100
+++ b/src/HOL/Tools/ATP/watcher.ML	Fri Mar 10 17:57:09 2006 +0100
@@ -26,7 +26,9 @@
     thm * string Array.array -> 
     TextIO.instream * TextIO.outstream * Posix.Process.pid
 val killWatcher : Posix.Process.pid -> unit
+val killChild  : ('a, 'b) Unix.proc -> OS.Process.status
 val setting_sep : char
+val reapAll : unit -> unit
 end
 
 
@@ -227,8 +229,8 @@
 			    (childIn, toParentStr, ppid, file, th, sgno,names_arr)  
 		     | _ => (trace ("\nBad prover! " ^ prover); true) )
 		in
-		 if childDone (*child has found a proof and transferred it*)
-		 then (Unix.reap proc_handle; OS.FileSys.remove file;
+		 if childDone (*ATP has reported back (with success OR failure)*)
+		 then (Unix.reap proc_handle;  OS.FileSys.remove file;
 		       check children)
 		 else child :: check children
 	      end
@@ -320,9 +322,10 @@
 (* Start a watcher and set up signal handlers             *)
 (**********************************************************)
 
-fun reapAll s = (*Signal handler to tidy away dead processes*)
+(*Signal handler to tidy away zombie processes*)
+fun reapAll() = 
      (case Posix.Process.waitpid_nh(Posix.Process.W_ANY_CHILD, []) of
-	  SOME _ => reapAll s | NONE => ()) 
+	  SOME _ => reapAll() | NONE => ()) 
      handle OS.SysErr _ => ()
 
 (*FIXME: does the main process need something like this?