src/HOL/Tools/ATP/watcher.ML
author paulson
Tue Oct 04 09:59:01 2005 +0200 (2005-10-04)
changeset 17746 af59c748371d
parent 17716 89932e53f31d
child 17764 fde495b9e24b
permissions -rw-r--r--
fixed the ascii-armouring of goalstring
     1 (*  Title:      Watcher.ML
     2     ID:         $Id$
     3     Author:     Claire Quigley
     4     Copyright   2004  University of Cambridge
     5  *)
     6 
     7  (***************************************************************************)
     8  (*  The watcher process starts a resolution process when it receives a     *)
     9 (*  message from Isabelle                                                  *)
    10 (*  Signals Isabelle, puts output of child into pipe to Isabelle,          *)
    11 (*  and removes dead processes.  Also possible to kill all the resolution  *)
    12 (*  processes currently running.                                           *)
    13 (*  Hardwired version of where to pick up the tptp files for the moment    *)
    14 (***************************************************************************)
    15 
    16 signature WATCHER =
    17 sig
    18 
    19 (*  Send request to Watcher for multiple spasses to be called for filenames in arg       *)
    20 (* callResProvers (outstreamtoWatcher, prover name,prover-command, (settings,file) list *)
    21 
    22 val callResProvers :
    23     TextIO.outstream * (string*string*string*string*string) list 
    24     -> unit
    25 
    26 (* Send message to watcher to kill currently running resolution provers *)
    27 val callSlayer : TextIO.outstream -> unit
    28 
    29 (* Start a watcher and set up signal handlers             *)
    30 val createWatcher : 
    31     thm * (ResClause.clause * thm) Array.array -> 
    32     TextIO.instream * TextIO.outstream * Posix.Process.pid
    33 
    34 (* Kill watcher process                                   *)
    35 val killWatcher : Posix.Process.pid -> unit
    36 val killWatcher' : int -> unit
    37 end
    38 
    39 
    40 
    41 structure Watcher: WATCHER =
    42 struct
    43 
    44 open Recon_Transfer
    45 
    46 val goals_being_watched = ref 0;
    47 
    48 val trace_path = Path.basic "watcher_trace";
    49 
    50 fun trace s = if !Output.show_debug_msgs then File.append (File.tmp_path trace_path) s 
    51               else ();
    52 
    53 (*  The result of calling createWatcher  *)
    54 datatype proc = PROC of {
    55         pid : Posix.Process.pid,
    56         instr : TextIO.instream,
    57         outstr : TextIO.outstream
    58       };
    59 
    60 (*  The result of calling executeToList  *)
    61 datatype cmdproc = CMDPROC of {
    62         prover: string,       (* Name of the resolution prover used, e.g. Vampire*)
    63         cmd:  string,         (* The file containing the goal for res prover to prove *)     
    64         goalstring: string,   (* string representation of subgoal*) 
    65         proc_handle : (TextIO.instream,TextIO.outstream) Unix.proc,
    66         instr : TextIO.instream,   (*  Input stream to child process *)
    67         outstr : TextIO.outstream};  (*  Output stream from child process *)
    68 
    69 type signal = Posix.Signal.signal
    70 datatype exit_status = datatype Posix.Process.exit_status
    71 
    72 val fromStatus = Posix.Process.fromStatus
    73 
    74 fun reap(pid, instr, outstr) =
    75   let val u = TextIO.closeIn instr;
    76       val u = TextIO.closeOut outstr;
    77       val (_, status) = Posix.Process.waitpid(Posix.Process.W_CHILD pid, [])
    78   in status end
    79 
    80 fun fdReader (name : string, fd : Posix.IO.file_desc) =
    81 	  Posix.IO.mkTextReader {initBlkMode = true,name = name,fd = fd };
    82 
    83 fun fdWriter (name, fd) =
    84           Posix.IO.mkTextWriter {
    85 	      appendMode = false,
    86               initBlkMode = true,
    87               name = name,  
    88               chunkSize=4096,
    89               fd = fd};
    90 
    91 fun openOutFD (name, fd) =
    92 	  TextIO.mkOutstream (
    93 	    TextIO.StreamIO.mkOutstream (
    94 	      fdWriter (name, fd), IO.BLOCK_BUF));
    95 
    96 fun openInFD (name, fd) =
    97 	  TextIO.mkInstream (
    98 	    TextIO.StreamIO.mkInstream (
    99 	      fdReader (name, fd), ""));
   100 
   101 fun childInfo (PROC{pid,instr,outstr }) = (pid,(instr,outstr));
   102 
   103 fun cmdstreamsOf (CMDPROC{instr,outstr,...}) = (instr, outstr);
   104 
   105 fun cmdInStream (CMDPROC{instr,outstr,...}) = instr;
   106 
   107 fun cmdchildInfo (CMDPROC{prover,cmd,proc_handle,goalstring,instr,outstr}) = 
   108   (prover,(cmd, (instr,outstr)));
   109 
   110 fun cmdchildHandle (CMDPROC{prover,cmd,goalstring,proc_handle,instr,outstr})  = 
   111   proc_handle;
   112 
   113 fun cmdProver (CMDPROC{prover,cmd,goalstring,proc_handle,instr,outstr})  =
   114   prover;
   115 
   116 fun cmdGoal (CMDPROC{prover,cmd,goalstring,proc_handle,instr,outstr})  =
   117   goalstring;
   118 
   119 
   120 (*    gets individual args from instream and concatenates them into a list      *)
   121 fun getArgs (fromParentStr, toParentStr, ys) =  
   122   let val thisLine = TextIO.input fromParentStr
   123   in ys@[thisLine] end
   124 
   125                             
   126 (*  Send request to Watcher for a vampire to be called for filename in arg      *)
   127                    
   128 fun callResProver (toWatcherStr,  arg) = 
   129       (TextIO.output (toWatcherStr, arg^"\n"); 
   130        TextIO.flushOut toWatcherStr)
   131 
   132 (*****************************************************************************************)
   133 (*  Send request to Watcher for multiple provers to be called for filenames in arg       *)
   134 (*  need to do the dfg stuff in the watcher, not here! send over the clasimp and stuff files too*)
   135 (*****************************************************************************************)
   136 
   137     
   138 (*Uses the $-character to separate items sent to watcher*)
   139 fun callResProvers (toWatcherStr,  []) = 
   140       (TextIO.output (toWatcherStr, "End of calls\n");  TextIO.flushOut toWatcherStr)
   141 |   callResProvers (toWatcherStr,
   142                     (prover,goalstring, proverCmd,settings, 
   143                      probfile)  ::  args) =
   144       let val _ = trace (space_implode "\n" 
   145 		         (["\ncallResProvers:",prover,goalstring,proverCmd,settings,
   146 			  probfile]))
   147       in TextIO.output (toWatcherStr,    
   148                         prover^"$"^proverCmd^"$"^ settings^"$"^probfile^"$\n");
   149          TextIO.output (toWatcherStr, String.toString goalstring^"\n");
   150               (*goalstring is a single string literal, with all specials escaped.*)
   151          goals_being_watched := (!goals_being_watched) + 1;
   152 	 TextIO.flushOut toWatcherStr;
   153 	 callResProvers (toWatcherStr,args)
   154       end   
   155                                                 
   156                                     
   157  
   158 (**************************************************************)
   159 (* Send message to watcher to kill currently running vampires *)
   160 (**************************************************************)
   161 
   162 fun callSlayer toWatcherStr = (TextIO.output (toWatcherStr, "Kill vampires\n"); 
   163                             TextIO.flushOut toWatcherStr)
   164 
   165                     
   166 (**************************************************************)
   167 (* Get commands from Isabelle                                 *)
   168 (**************************************************************)
   169 fun getCmds (toParentStr,fromParentStr, cmdList) = 
   170   let val thisLine = TextIO.inputLine fromParentStr 
   171       val _ = trace("\nGot command from parent: " ^ thisLine)
   172   in
   173      if thisLine = "End of calls\n" orelse thisLine = "" then cmdList
   174      else if thisLine = "Kill children\n"
   175      then (TextIO.output (toParentStr,thisLine ); 
   176 	   TextIO.flushOut toParentStr;
   177 	   (("","","Kill children",[],"")::cmdList)  )
   178      else
   179        let val [prover,proverCmd,settingstr,probfile,_] = 
   180                    String.tokens (fn c => c = #"$") thisLine
   181            val settings = String.tokens (fn c => c = #"%") settingstr
   182 	   val goalstring = TextIO.inputLine fromParentStr 
   183        in
   184            trace ("\nprover: " ^ prover ^ "  prover path: " ^ proverCmd^
   185                   "  problem file: " ^ probfile ^ 
   186 		  "\ngoalstring:  "^goalstring);
   187            getCmds (toParentStr, fromParentStr, 
   188                     (prover, goalstring, proverCmd, settings, probfile)::cmdList) 
   189        end
   190   end
   191 	    
   192                                                                   
   193 (**************************************************************)
   194 (*  Get Io-descriptor for polling of an input stream          *)
   195 (**************************************************************)
   196 
   197 fun getInIoDesc someInstr = 
   198     let val (rd, buf) = TextIO.StreamIO.getReader(TextIO.getInstream someInstr)
   199         val _ = TextIO.output (TextIO.stdOut, buf)
   200         val ioDesc = 
   201 	    case rd
   202 	      of TextPrimIO.RD{ioDesc = SOME iod, ...} =>SOME iod
   203 	       | _ => NONE
   204      in (* since getting the reader will have terminated the stream, we need
   205 	 * to build a new stream. *)
   206 	TextIO.setInstream(someInstr, TextIO.StreamIO.mkInstream(rd, buf));
   207 	ioDesc
   208     end
   209 
   210 
   211 (*************************************)
   212 (*  Set up a Watcher Process         *)
   213 (*************************************)
   214 
   215 fun getProofCmd (a,c,d,e,f) = d
   216 
   217 (* for tracing: encloses each string element in brackets. *)
   218 val concat_with_and = space_implode " & " o map (enclose "(" ")");
   219 
   220 fun prems_string_of th =
   221   concat_with_and (map (Sign.string_of_term (sign_of_thm th)) (prems_of th))
   222 
   223 fun killChild proc = (Unix.kill(proc, Posix.Signal.kill); Unix.reap proc);
   224 
   225 fun killChildren procs = List.app (ignore o killChild) procs;
   226 
   227  (*************************************************************)
   228  (* take an instream and poll its underlying reader for input *)
   229  (*************************************************************)
   230  
   231  fun pollParentInput (fromParentIOD, fromParentStr, toParentStr) = 
   232    case OS.IO.pollDesc fromParentIOD of
   233       SOME pd =>
   234 	 (case OS.IO.poll ([OS.IO.pollIn pd], SOME (Time.fromSeconds 2)) of
   235 	      [] => NONE
   236 	    | pd''::_ => if OS.IO.isIn pd''
   237 	 	         then SOME (getCmds (toParentStr, fromParentStr, []))
   238 	 	         else NONE)
   239    | NONE => NONE;
   240 
   241 (*get the number of the subgoal from the filename: the last digit string*)
   242 fun number_from_filename s =
   243   case String.tokens (not o Char.isDigit) s of
   244       [] => (trace "\nWatcher could not read subgoal nunber!!"; raise ERROR)
   245     | numbers => valOf (Int.fromString (List.last numbers));
   246 
   247 fun setupWatcher (thm,clause_arr) = 
   248   let
   249     (** pipes for communication between parent and watcher **)
   250     val p1 = Posix.IO.pipe ()
   251     val p2 = Posix.IO.pipe ()
   252     fun closep () = 
   253 	 (Posix.IO.close (#outfd p1); 
   254 	  Posix.IO.close (#infd p1);
   255 	  Posix.IO.close (#outfd p2); 
   256 	  Posix.IO.close (#infd p2))
   257     (***********************************************************)
   258     (****** fork a watcher process and get it set up and going *)
   259     (***********************************************************)
   260     fun startWatcher procList =
   261      (case  Posix.Process.fork() (***************************************)
   262       of SOME pid =>  pid           (* parent - i.e. main Isabelle process *)
   263 				    (***************************************)
   264 
   265 				      (*************************)
   266        | NONE => let                  (* child - i.e. watcher  *)
   267 	  val oldchildin = #infd p1   (*************************)
   268 	  val fromParent = Posix.FileSys.wordToFD 0w0
   269 	  val oldchildout = #outfd p2
   270 	  val toParent = Posix.FileSys.wordToFD 0w1
   271 	  val fromParentIOD = Posix.FileSys.fdToIOD fromParent
   272 	  val fromParentStr = openInFD ("_exec_in_parent", fromParent)
   273 	  val toParentStr = openOutFD ("_exec_out_parent", toParent)
   274 	  val _ = debug ("subgoals forked to startWatcher: "^ prems_string_of thm);
   275 	 
   276 	  fun pollChildInput fromStr = 
   277 	     case getInIoDesc fromStr of
   278 	       SOME iod => 
   279 		 (case OS.IO.pollDesc iod of
   280 		    SOME pd =>
   281 			let val pd' = OS.IO.pollIn pd
   282 			in
   283 			  case OS.IO.poll ([pd'], SOME (Time.fromSeconds 2)) of
   284 			      [] => false
   285 			    | pd''::_ => OS.IO.isIn pd''
   286 			end
   287 		   | NONE => false)
   288 	     | NONE => false
   289 
   290 
   291 	  (* Check all ATP processes currently running for output                 *)
   292 	  fun checkChildren ([], toParentStr) = []  (* no children to check *)
   293 	  |   checkChildren (childProc::otherChildren, toParentStr) = 
   294 	       let val _ = trace ("\nIn check child, length of queue:"^
   295 			          Int.toString (length (childProc::otherChildren)))
   296 		   val (childInput,childOutput) = cmdstreamsOf childProc
   297 		   val child_handle = cmdchildHandle childProc
   298 		   (* childCmd is the file that the problem is in *)
   299 		   val childCmd = fst(snd (cmdchildInfo childProc))
   300 		   val _ = trace ("\nchildCmd = " ^ childCmd)
   301 		   val sg_num = number_from_filename childCmd
   302 		   val childIncoming = pollChildInput childInput
   303 		   val parentID = Posix.ProcEnv.getppid()
   304 		   val prover = cmdProver childProc
   305 		   val prems_string = prems_string_of thm
   306 		   val goalstring = cmdGoal childProc							
   307 	       in 
   308 		 trace("\nsubgoals forked to checkChildren: " ^ goalstring);
   309 		 if childIncoming
   310 		 then 
   311 		   (* check here for prover label on child*)
   312 		   let val _ = trace ("\nInput available from child: " ^
   313 				      childCmd ^ 
   314 				      "\ngoalstring is " ^ goalstring)
   315 		       val childDone = (case prover of
   316 			   "vampire" => AtpCommunication.checkVampProofFound(childInput, toParentStr, parentID,goalstring, childCmd, clause_arr)  
   317 			    | "E" => AtpCommunication.checkEProofFound(childInput, toParentStr, parentID,goalstring, childCmd, clause_arr)             
   318 			  |"spass" => AtpCommunication.checkSpassProofFound(childInput, toParentStr, parentID,goalstring, childCmd, thm, sg_num,clause_arr)  )
   319 		    in
   320 		     if childDone
   321 		     then (* child has found a proof and transferred it *)
   322 			(* Remove this child and go on to check others*)
   323 			(Unix.reap child_handle;
   324 			 OS.FileSys.remove childCmd;
   325 			 checkChildren(otherChildren, toParentStr))
   326 		     else (* Keep this child and go on to check others  *)
   327 		       childProc :: checkChildren (otherChildren, toParentStr)
   328 		  end
   329 		else (trace "\nNo child output";
   330 		      childProc::(checkChildren (otherChildren, toParentStr)))
   331 	       end
   332 
   333 	
   334      (********************************************************************)                  
   335      (* call resolution processes                                        *)
   336      (* settings should be a list of strings                             *)
   337      (* e.g. ["-t 300", "-m 100000"]         (TextIO.input instr)^                            *)
   338      (* takes list of (string, string, string list, string)list proclist *)
   339      (********************************************************************)
   340 
   341 
   342 (*** add subgoal id num to this *)
   343 	fun execCmds  [] procList = procList
   344 	|   execCmds  ((prover, goalstring,proverCmd,settings,file)::cmds) procList  =
   345 	      let val _ = trace 
   346 	                    (space_implode "\n" 
   347 	                      (["\nAbout to execute command for goal:",
   348 	                        goalstring, proverCmd] @ settings @
   349 	                       [file, Date.toString(Date.fromTimeLocal(Time.now()))]))
   350 	          val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = 
   351 		       (Unix.execute(proverCmd, (settings@[file])))
   352 		  val (instr, outstr) = Unix.streamsOf childhandle
   353 		  val newProcList = (CMDPROC{
   354 				       prover = prover,
   355 				       cmd = file,
   356 				       goalstring = goalstring,
   357 				       proc_handle = childhandle,
   358 				       instr = instr,
   359 				       outstr = outstr }) :: procList
   360      
   361 		  val _ = trace ("\nFinished at " ^
   362 			         Date.toString(Date.fromTimeLocal(Time.now())))
   363 	      in execCmds cmds newProcList end
   364 
   365 
   366      (****************************************)                  
   367      (* call resolution processes remotely   *)
   368      (* settings should be a list of strings *)
   369      (* e.g. ["-t300", "-m100000"]         *)
   370      (****************************************)
   371 
   372       (*  fun execRemoteCmds  [] procList = procList
   373 	|   execRemoteCmds ((prover, goalstring,proverCmd ,settings,file)::cmds) procList  =  
   374 	      let val  newProcList =  mySshExecuteToList ("/usr/bin/ssh",([prover,goalstring,"-t", "shep"]@[proverCmd]@settings@[file]), procList)
   375 		  in
   376 		       execRemoteCmds  cmds newProcList
   377 		  end
   378 *)
   379 
   380      (**********************************************)                  
   381      (* Watcher Loop                               *)
   382      (**********************************************)
   383          val iterations_left = ref 500;  (*don't let it run forever*)
   384 
   385 	 fun keepWatching (procList) = 
   386 	   let fun loop procList =  
   387 		let val _ = trace ("\nCalling pollParentInput: " ^ 
   388 			           Int.toString (!iterations_left));
   389 		    val cmdsFromIsa = pollParentInput 
   390 		                       (fromParentIOD, fromParentStr, toParentStr)
   391 		in 
   392 		   OS.Process.sleep (Time.fromMilliseconds 100);
   393 		   iterations_left := !iterations_left - 1;
   394 		   if !iterations_left <= 0 
   395 		   then 
   396 		    (trace "\nTimeout: Killing proof processes";
   397 	             TextIO.output(toParentStr, "Timeout: Killing proof processes!\n");
   398 		     TextIO.flushOut toParentStr;
   399 		     killChildren (map cmdchildHandle procList);
   400 		     exit 0)
   401 		   else if isSome cmdsFromIsa
   402 		   then (*  deal with input from Isabelle *)
   403 		     if getProofCmd(hd(valOf cmdsFromIsa)) = "Kill children" 
   404 		     then 
   405 		       let val child_handles = map cmdchildHandle procList 
   406 		       in
   407 			  killChildren child_handles;
   408 			  loop []
   409 		       end
   410 		     else
   411 		       if length procList < 5     (********************)
   412 		       then                        (* Execute locally  *)
   413 			 let 
   414 			   val newProcList = execCmds (valOf cmdsFromIsa) procList
   415 			   val _ = Posix.ProcEnv.getppid()
   416 			   val _ = trace "\nJust execed a child"
   417 			   val newProcList' = checkChildren (newProcList, toParentStr) 
   418 			 in
   419 			   trace ("\nOff to keep watching: " ^ 
   420 			          Int.toString (!iterations_left));
   421 			   loop newProcList'
   422 			 end
   423 		       else  (* Execute remotely              *)
   424 			     (* (actually not remote for now )*)
   425 			 let 
   426 			   val newProcList = execCmds (valOf cmdsFromIsa) procList
   427 			   val _ = Posix.ProcEnv.getppid()
   428 			   val newProcList' =checkChildren (newProcList, toParentStr) 
   429 			 in
   430 			   loop newProcList'
   431 			 end
   432 		   else (* No new input from Isabelle *)
   433 		     let val newProcList = checkChildren (procList, toParentStr)
   434 		     in
   435 		       trace ("\nNo new input, still watching: " ^ 
   436 			      Int.toString (!iterations_left));
   437 		       loop newProcList
   438 		     end
   439 		 end
   440 	   in  
   441 	       loop procList
   442 	   end
   443 	   
   444 
   445 	   in
   446 	    (***************************)
   447 	    (*** Sort out pipes ********)
   448 	    (***************************)
   449 
   450 	     Posix.IO.close (#outfd p1);
   451 	     Posix.IO.close (#infd p2);
   452 	     Posix.IO.dup2{old = oldchildin, new = fromParent};
   453 	     Posix.IO.close oldchildin;
   454 	     Posix.IO.dup2{old = oldchildout, new = toParent};
   455 	     Posix.IO.close oldchildout;
   456 
   457 	     (***************************)
   458 	     (* start the watcher loop  *)
   459 	     (***************************)
   460 	     keepWatching (procList);
   461 	     (****************************************************************************)
   462 (* fake return value - actually want the watcher to loop until killed *)
   463 	     (****************************************************************************)
   464 	     Posix.Process.wordToPid 0w0
   465 	   end);
   466      (* end case *)
   467 
   468 
   469     val _ = TextIO.flushOut TextIO.stdOut
   470 
   471     (*******************************)
   472     (***  set watcher going ********)
   473     (*******************************)
   474 
   475     val procList = []
   476     val pid = startWatcher procList
   477     (**************************************************)
   478     (* communication streams to watcher               *)
   479     (**************************************************)
   480 
   481     val instr = openInFD ("_exec_in", #infd p2)
   482     val outstr = openOutFD ("_exec_out", #outfd p1)
   483     
   484   in
   485    (*******************************)
   486    (* close the child-side fds    *)
   487    (*******************************)
   488     Posix.IO.close (#outfd p2);
   489     Posix.IO.close (#infd p1);
   490     (* set the fds close on exec *)
   491     Posix.IO.setfd (#infd p2, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   492     Posix.IO.setfd (#outfd p1, Posix.IO.FD.flags [Posix.IO.FD.cloexec]);
   493      
   494    (*******************************)
   495    (* return value                *)
   496    (*******************************)
   497     PROC{pid = pid, instr = instr, outstr = outstr}
   498   end;
   499 
   500 
   501 
   502 (**********************************************************)
   503 (* Start a watcher and set up signal handlers             *)
   504 (**********************************************************)
   505 
   506 fun killWatcher pid = Posix.Process.kill(Posix.Process.K_PROC pid, Posix.Signal.kill);
   507 
   508 val killWatcher' = killWatcher o ResLib.pidOfInt;
   509 
   510 fun reapWatcher(pid, instr, outstr) =
   511   (TextIO.closeIn instr; TextIO.closeOut outstr;
   512    Posix.Process.waitpid(Posix.Process.W_CHILD pid, []); ())
   513 
   514 fun createWatcher (thm, clause_arr) =
   515  let val (childpid,(childin,childout)) = childInfo (setupWatcher(thm,clause_arr))
   516      fun decr_watched() =
   517 	  (goals_being_watched := !goals_being_watched - 1;
   518 	   if !goals_being_watched = 0
   519 	   then 
   520 	     (debug ("\nReaping a watcher, childpid = "^
   521 		     LargeWord.toString (Posix.Process.pidToWord childpid));
   522 	      killWatcher childpid; reapWatcher (childpid,childin, childout))
   523 	    else ())
   524      val _ = debug ("subgoals forked to createWatcher: "^ prems_string_of thm);
   525      fun proofHandler n = 
   526        let val outcome = TextIO.inputLine childin
   527 	   val goalstring = valOf (String.fromString (TextIO.inputLine childin))
   528 	   val _ = debug ("In signal handler. outcome = \"" ^ outcome ^ 
   529 		        "\"\ngoalstring = " ^ goalstring ^
   530 		        "\ngoals_being_watched: "^  Int.toString (!goals_being_watched))
   531        in 
   532 	 if String.isPrefix "[" outcome (*indicates a proof reconstruction*)
   533 	 then (priority (Recon_Transfer.apply_res_thm outcome goalstring);
   534 	       decr_watched())
   535 	 else if String.isPrefix "Invalid" outcome
   536 	 then (priority ("Subgoal is not provable:\n" ^ goalstring);
   537 	       decr_watched())
   538 	 else if String.isPrefix "Failure" outcome
   539 	 then (priority ("Proof attempt failed:\n" ^ goalstring);
   540 	       decr_watched()) 
   541 	(* print out a list of rules used from clasimpset*)
   542 	 else if String.isPrefix "Success" outcome
   543 	 then (priority (outcome ^ goalstring);
   544 	       decr_watched())
   545 	  (* if proof translation failed *)
   546 	 else if String.isPrefix "Translation failed" outcome
   547 	 then (priority (outcome ^ goalstring);
   548 	       decr_watched())
   549 	 else (priority "System error in proof handler";
   550 	       decr_watched())
   551        end
   552  in IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE proofHandler);
   553     (childin, childout, childpid)
   554   end
   555 
   556 end (* structure Watcher *)