Now uses File.write and File.append
authorpaulson
Fri May 27 12:12:05 2005 +0200 (2005-05-27)
changeset 16100f80fc4bff933
parent 16099 c5882ca551dd
child 16101 37471d84d353
Now uses File.write and File.append
src/HOL/Tools/ATP/watcher.ML
     1.1 --- a/src/HOL/Tools/ATP/watcher.ML	Fri May 27 01:30:27 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/watcher.ML	Fri May 27 12:12:05 2005 +0200
     1.3 @@ -153,21 +153,20 @@
     1.4  (*****************************************************************************************)
     1.5  
     1.6  (* need to modify to send over hyps file too *)
     1.7 -fun callResProvers (toWatcherStr,  []) = (sendOutput (toWatcherStr, "End of calls\n"); 
     1.8 -                                     TextIO.flushOut toWatcherStr)
     1.9 +fun callResProvers (toWatcherStr,  []) =
    1.10 +      (sendOutput (toWatcherStr, "End of calls\n"); 
    1.11 +       TextIO.flushOut toWatcherStr)
    1.12  |   callResProvers (toWatcherStr,(prover,thmstring,goalstring, proverCmd,settings,clasimpfile, axfile, hypsfile,probfile)::args) =
    1.13        let val dfg_dir = File.tmp_path (Path.basic "dfg"); 
    1.14  	 (*** need to check here if the directory exists and, if not, create it***)
    1.15 -	  val  outfile = TextIO.openAppend(File.sysify_path
    1.16 -				(File.tmp_path (Path.basic"thmstring_in_watcher")));                                                                         
    1.17 -	  val _ = TextIO.output (outfile, 
    1.18 -			(thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^"\n"))
    1.19 -	  val _ =  TextIO.closeOut outfile
    1.20 +	  val _ = File.append (File.tmp_path (Path.basic"thmstring_in_watcher"))                                                                     
    1.21 +	              (thmstring^"\n goals_watched"^(string_of_int(!goals_being_watched))^"\n")
    1.22  	 (*** want to cat clasimp ax hyps prob, then send the resulting file to tptp2x ***)
    1.23  	  val probID = ReconOrderClauses.last(explode probfile)
    1.24  	  val wholefile = File.tmp_path (Path.basic ("ax_prob_"^probID))
    1.25  	  (*** only include problem and clasimp for the moment, not sure how to refer to ***)
    1.26  	  (*** hyps/local axioms just now                                                ***)
    1.27 +          (*FIXME: find a way that works for SML/NJ too: it regards > as a filename!*)
    1.28  	  val whole_prob_file = Unix.execute("/bin/cat", [clasimpfile,(*,axfile, hypsfile,*)probfile,  ">", (File.sysify_path wholefile)])
    1.29  	  val dfg_create = if File.exists dfg_dir 
    1.30  			   then warning("dfg dir exists")
    1.31 @@ -235,26 +234,25 @@
    1.32                                       getSettings rest (settings@[(implode set)])
    1.33                                   end
    1.34  
    1.35 -fun separateFields str = let val (prover, rest) = takeUntil "*" str []
    1.36 -                              val prover = implode prover
    1.37 -                              val (thmstring, rest) =  takeUntil "*" rest []
    1.38 -                              val thmstring = implode thmstring
    1.39 -                              val (goalstring, rest) =  takeUntil "*" rest []
    1.40 -                              val goalstring = implode goalstring
    1.41 -                              val (proverCmd, rest ) =  takeUntil "*" rest []
    1.42 -                              val proverCmd = implode proverCmd
    1.43 -                              
    1.44 -                              val (settings, rest) =  takeUntil "*" rest []
    1.45 -                              val settings = getSettings settings []
    1.46 -                              val (file, rest) =  takeUntil "*" rest []
    1.47 -                              val file = implode file
    1.48 -                              val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "sep_comms")));                                                                                    
    1.49 -                              val _ = TextIO.output (outfile,(prover^thmstring^goalstring^proverCmd^file) )
    1.50 -                              val _ =  TextIO.closeOut outfile
    1.51 -                              
    1.52 -                          in
    1.53 -                             (prover,thmstring,goalstring, proverCmd, settings, file)
    1.54 -                          end
    1.55 +fun separateFields str =
    1.56 +  let val (prover, rest) = takeUntil "*" str []
    1.57 +      val prover = implode prover
    1.58 +      val (thmstring, rest) =  takeUntil "*" rest []
    1.59 +      val thmstring = implode thmstring
    1.60 +      val (goalstring, rest) =  takeUntil "*" rest []
    1.61 +      val goalstring = implode goalstring
    1.62 +      val (proverCmd, rest ) =  takeUntil "*" rest []
    1.63 +      val proverCmd = implode proverCmd
    1.64 +      
    1.65 +      val (settings, rest) =  takeUntil "*" rest []
    1.66 +      val settings = getSettings settings []
    1.67 +      val (file, rest) =  takeUntil "*" rest []
    1.68 +      val file = implode file
    1.69 +      val _ = File.write (File.tmp_path (Path.basic "sep_comms"))
    1.70 +                (prover^thmstring^goalstring^proverCmd^file) 
    1.71 +  in
    1.72 +     (prover,thmstring,goalstring, proverCmd, settings, file)
    1.73 +  end
    1.74  
    1.75   
    1.76  
    1.77 @@ -277,26 +275,26 @@
    1.78  (**************************************************************)
    1.79  
    1.80  fun getCmds (toParentStr,fromParentStr, cmdList) = 
    1.81 -                                       let val thisLine = TextIO.inputLine fromParentStr 
    1.82 -                                       in
    1.83 -                                          (if (thisLine = "End of calls\n") 
    1.84 -                                           then 
    1.85 -                                              (cmdList)
    1.86 -                                           else if (thisLine = "Kill children\n") 
    1.87 -                                                then 
    1.88 -                                                    (   TextIO.output (toParentStr,thisLine ); 
    1.89 -                                                        TextIO.flushOut toParentStr;
    1.90 -                                                      (("","","","Kill children",[],"")::cmdList)
    1.91 -                                                     )
    1.92 -                                              else (let val thisCmd = getCmd (thisLine) (* thisCmd = (prover,thmstring,proverCmd, settings, file)*)
    1.93 -                                                    in
    1.94 -                                                      (*TextIO.output (toParentStr, thisCmd); 
    1.95 -                                                        TextIO.flushOut toParentStr;*)
    1.96 -                                                        getCmds (toParentStr,fromParentStr, (thisCmd::cmdList))
    1.97 -                                                    end
    1.98 -                                                    )
    1.99 -                                            )
   1.100 -                                        end
   1.101 +       let val thisLine = TextIO.inputLine fromParentStr 
   1.102 +       in
   1.103 +	  (if (thisLine = "End of calls\n") 
   1.104 +	   then 
   1.105 +	      (cmdList)
   1.106 +	   else if (thisLine = "Kill children\n") 
   1.107 +		then 
   1.108 +		    (   TextIO.output (toParentStr,thisLine ); 
   1.109 +			TextIO.flushOut toParentStr;
   1.110 +		      (("","","","Kill children",[],"")::cmdList)
   1.111 +		     )
   1.112 +	      else (let val thisCmd = getCmd (thisLine) (* thisCmd = (prover,thmstring,proverCmd, settings, file)*)
   1.113 +		    in
   1.114 +		      (*TextIO.output (toParentStr, thisCmd); 
   1.115 +			TextIO.flushOut toParentStr;*)
   1.116 +			getCmds (toParentStr,fromParentStr, (thisCmd::cmdList))
   1.117 +		    end
   1.118 +		    )
   1.119 +	    )
   1.120 +	end
   1.121                                      
   1.122                                      
   1.123  (**************************************************************)
   1.124 @@ -448,20 +446,15 @@
   1.125  			val sign = sign_of_thm thm
   1.126  			val prems = prems_of thm
   1.127  			val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
   1.128 -			val _ = (warning ("subgoals forked to checkChildren: "^prems_string));
   1.129 -			val goalstring = cmdGoal childProc
   1.130 -									       
   1.131 -			val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "child_comms")));  
   1.132 -			val _ = TextIO.output (outfile,(prover^thmstring^goalstring^childCmd) )
   1.133 -			val _ =  TextIO.closeOut outfile
   1.134 +			val _ = warning("subgoals forked to checkChildren: "^prems_string)
   1.135 +			val goalstring = cmdGoal childProc							
   1.136 +			val _ = File.write (File.tmp_path (Path.basic "child_comms")) 
   1.137 +			           (prover^thmstring^goalstring^childCmd)
   1.138  		    in 
   1.139  		      if (isSome childIncoming) 
   1.140  		      then 
   1.141  			  (* check here for prover label on child*)
   1.142 -			   
   1.143 -			  let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "child_incoming")));  
   1.144 -			val _ = TextIO.output (outfile,(("subgoals forked to checkChildren: "^prems_string)^prover^thmstring^goalstring^childCmd) )
   1.145 -			val _ =  TextIO.closeOut outfile
   1.146 +			  let val _ = File.write (File.tmp_path (Path.basic "child_incoming"))  ("subgoals forked to checkChildren: "^prems_string^prover^thmstring^goalstring^childCmd) 
   1.147  		      val childDone = (case prover of
   1.148  	    (* "vampire" => startVampireTransfer(childInput, toParentStr, parentID, childCmd)                                               |*)"spass" => (checkSpassProofFound(childInput, toParentStr, parentID,thmstring,goalstring, childCmd, thm, sg_num,clause_arr, num_of_clauses)     ) )
   1.149  			   in
   1.150 @@ -482,12 +475,8 @@
   1.151  				 (childProc::(checkChildren (otherChildren, toParentStr)))
   1.152  			 end
   1.153  		       else
   1.154 -			   let val  outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "child_incoming")));  
   1.155 -			val _ = TextIO.output (outfile,"No child output " )
   1.156 -			val _ =  TextIO.closeOut outfile
   1.157 -			 in
   1.158 -			    (childProc::(checkChildren (otherChildren, toParentStr)))
   1.159 -			 end
   1.160 +			 (File.append (File.tmp_path (Path.basic "child_incoming")) "No child output ";
   1.161 +			  childProc::(checkChildren (otherChildren, toParentStr)))
   1.162  		    end
   1.163  
   1.164  	     
   1.165 @@ -502,38 +491,36 @@
   1.166  (*** add subgoal id num to this *)
   1.167  	     fun execCmds  [] procList = procList
   1.168  	     |   execCmds  ((prover, thmstring,goalstring,proverCmd,settings,file)::cmds) procList  = 
   1.169 -					       if (prover = "spass") 
   1.170 -					       then 
   1.171 -						   let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file])))
   1.172 -						       val (instr, outstr)=Unix.streamsOf childhandle
   1.173 -						       val newProcList =    (((CMDPROC{
   1.174 -									    prover = prover,
   1.175 -									    cmd = file,
   1.176 -									    thmstring = thmstring,
   1.177 -									    goalstring = goalstring,
   1.178 -									    proc_handle = childhandle,
   1.179 -									    instr = instr,
   1.180 -									    outstr = outstr })::procList))
   1.181 -							val  outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "exec_child")));  
   1.182 -					  val _ = TextIO.output (outfile,"executing command for goal:"^goalstring^proverCmd^(concat settings)^file )
   1.183 -					  val _ =  TextIO.closeOut outfile
   1.184 -						   in
   1.185 -						      execCmds cmds newProcList
   1.186 -						   end
   1.187 -					       else 
   1.188 -						   let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file])))
   1.189 -						       val (instr, outstr)=Unix.streamsOf childhandle
   1.190 -						       val newProcList =    (((CMDPROC{
   1.191 -									    prover = prover,
   1.192 -									    cmd = file,
   1.193 -									    thmstring = thmstring,
   1.194 -									    goalstring = goalstring,
   1.195 -									    proc_handle = childhandle,
   1.196 -									    instr = instr,
   1.197 -									    outstr = outstr })::procList))
   1.198 -						   in
   1.199 -						      execCmds cmds newProcList
   1.200 -						   end
   1.201 +		   if (prover = "spass") 
   1.202 +		   then 
   1.203 +		       let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file])))
   1.204 +			   val (instr, outstr)=Unix.streamsOf childhandle
   1.205 +			   val newProcList =    (((CMDPROC{
   1.206 +						prover = prover,
   1.207 +						cmd = file,
   1.208 +						thmstring = thmstring,
   1.209 +						goalstring = goalstring,
   1.210 +						proc_handle = childhandle,
   1.211 +						instr = instr,
   1.212 +						outstr = outstr })::procList))
   1.213 +			    val _ = File.append (File.tmp_path (Path.basic "exec_child"))  ("executing command for goal:"^goalstring^proverCmd^(concat settings)^file)
   1.214 +		       in
   1.215 +			  execCmds cmds newProcList
   1.216 +		       end
   1.217 +		   else 
   1.218 +		       let val childhandle:(TextIO.instream,TextIO.outstream) Unix.proc  = (Unix.execute(proverCmd, (["-FullRed=0"]@settings@[file])))
   1.219 +			   val (instr, outstr)=Unix.streamsOf childhandle
   1.220 +			   val newProcList =    (((CMDPROC{
   1.221 +						prover = prover,
   1.222 +						cmd = file,
   1.223 +						thmstring = thmstring,
   1.224 +						goalstring = goalstring,
   1.225 +						proc_handle = childhandle,
   1.226 +						instr = instr,
   1.227 +						outstr = outstr })::procList))
   1.228 +		       in
   1.229 +			  execCmds cmds newProcList
   1.230 +		       end
   1.231  
   1.232  
   1.233  
   1.234 @@ -713,103 +700,83 @@
   1.235  		status
   1.236  	end
   1.237  
   1.238 -fun createWatcher (thm,clause_arr, ( num_of_clauses:int)) = let val mychild = childInfo (setupWatcher(thm,clause_arr,  num_of_clauses))
   1.239 -			   val streams =snd mychild
   1.240 -                           val childin = fst streams
   1.241 -                           val childout = snd streams
   1.242 -                           val childpid = fst mychild
   1.243 -                           val sign = sign_of_thm thm
   1.244 -                           val prems = prems_of thm
   1.245 -                           val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
   1.246 -                           val _ = (warning ("subgoals forked to createWatcher: "^prems_string));
   1.247 -                           fun vampire_proofHandler (n) =
   1.248 -                           (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.249 -                           getVampInput childin; Pretty.writeln(Pretty.str  (oct_char "361"));() )               
   1.250 -                          
   1.251 -
   1.252 -fun spass_proofHandler (n) = (
   1.253 -                                 let  val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_signal1")));
   1.254 -                                      val _ = TextIO.output (outfile, ("In signal handler now\n"))
   1.255 -                                      val _ =  TextIO.closeOut outfile
   1.256 -                                      val (reconstr, thmstring, goalstring) = getSpassInput childin
   1.257 -                                      val  outfile = TextIO.openAppend(File.sysify_path(File.tmp_path (Path.basic "foo_signal")));
   1.258 -
   1.259 -                                      val _ = TextIO.output (outfile, ("In signal handler  "^reconstr^thmstring^goalstring^"goals_being_watched is: "^(string_of_int (!goals_being_watched))))
   1.260 -                                      val _ =  TextIO.closeOut outfile
   1.261 -                                      in          (* if a proof has been found and sent back as a reconstruction proof *)
   1.262 -                                                  if ( (substring (reconstr, 0,1))= "[")
   1.263 -                                                  then 
   1.264 +fun createWatcher (thm,clause_arr, ( num_of_clauses:int)) = 
   1.265 +  let val mychild = childInfo (setupWatcher(thm,clause_arr,  num_of_clauses))
   1.266 +      val streams =snd mychild
   1.267 +      val childin = fst streams
   1.268 +      val childout = snd streams
   1.269 +      val childpid = fst mychild
   1.270 +      val sign = sign_of_thm thm
   1.271 +      val prems = prems_of thm
   1.272 +      val prems_string =  Meson.concat_with_and (map (Sign.string_of_term sign) prems) 
   1.273 +      val _ = (warning ("subgoals forked to createWatcher: "^prems_string));
   1.274 +      fun vampire_proofHandler (n) =
   1.275 +	    (Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.276 +	    getVampInput childin; Pretty.writeln(Pretty.str  (oct_char "361"));() )               
   1.277 +     
   1.278  
   1.279 -                                                            (
   1.280 -                                                                 Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.281 -                                                                 Recon_Transfer.apply_res_thm reconstr goalstring;
   1.282 -                                                                 Pretty.writeln(Pretty.str  (oct_char "361"));
   1.283 -                                                                 
   1.284 -                                                                 goals_being_watched := ((!goals_being_watched) - 1);
   1.285 -                                                         
   1.286 -                                                                 if ((!goals_being_watched) = 0)
   1.287 -                                                                 then 
   1.288 -                                                                    (let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_reap_found")));
   1.289 -                                                                         val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   1.290 -                                                                         val _ =  TextIO.closeOut outfile
   1.291 -                                                                     in
   1.292 -                                                                         reapWatcher (childpid,childin, childout); ()
   1.293 -                                                                     end)
   1.294 -                                                                 else
   1.295 -                                                                    ()
   1.296 -                                                            )
   1.297 -                                                    (* if there's no proof, but a message from Spass *)
   1.298 -                                                    else if ((substring (reconstr, 0,5))= "SPASS")
   1.299 -                                                         then
   1.300 -                                                                 (
   1.301 -                                                                     goals_being_watched := (!goals_being_watched) -1;
   1.302 -                                                                     Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.303 -                                                                      Pretty.writeln(Pretty.str (goalstring^reconstr));
   1.304 -                                                                      Pretty.writeln(Pretty.str  (oct_char "361"));
   1.305 -                                                                      if (!goals_being_watched = 0)
   1.306 -                                                                      then 
   1.307 -                                                                          (let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_reap_comp")));
   1.308 -                                                                               val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   1.309 -                                                                               val _ =  TextIO.closeOut outfile
   1.310 -                                                                           in
   1.311 -                                                                              reapWatcher (childpid,childin, childout); ()
   1.312 -                                                                           end )
   1.313 -                                                                      else
   1.314 -                                                                         ()
   1.315 -                                                                )
   1.316 -                                                          (* if proof translation failed *)
   1.317 -                                                          else if ((substring (reconstr, 0,5)) = "Proof")
   1.318 -                                                               then 
   1.319 -                                                                   (
   1.320 -                                                                     goals_being_watched := (!goals_being_watched) -1;
   1.321 -                                                                     Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.322 -                                                                      Pretty.writeln(Pretty.str (goalstring^reconstr));
   1.323 -                                                                      Pretty.writeln(Pretty.str  (oct_char "361"));
   1.324 -                                                                      if (!goals_being_watched = 0)
   1.325 -                                                                      then 
   1.326 -                                                                          (let val  outfile = TextIO.openOut(File.sysify_path(File.tmp_path (Path.basic "foo_reap_comp")));
   1.327 -                                                                               val _ = TextIO.output (outfile, ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n"))
   1.328 -                                                                               val _ =  TextIO.closeOut outfile
   1.329 -                                                                           in
   1.330 -                                                                              reapWatcher (childpid,childin, childout); ()
   1.331 -                                                                           end )
   1.332 -                                                                      else
   1.333 -                                                                         ()
   1.334 -                                                                )
   1.335 +      fun spass_proofHandler (n) = (
   1.336 +	let val _ = File.write (File.tmp_path (Path.basic "foo_signal1")) "In signal handler now\n"
   1.337 +	    val (reconstr, thmstring, goalstring) = getSpassInput childin
   1.338 +	    val _ = File.append (File.tmp_path (Path.basic "foo_signal"))
   1.339 +	              ("In signal handler  "^reconstr^thmstring^goalstring^"goals_being_watched is: "^(string_of_int (!goals_being_watched)))
   1.340 +        in (* if a proof has been found and sent back as a reconstruction proof *)
   1.341 +	  if ( (substring (reconstr, 0,1))= "[")
   1.342 +	  then 
   1.343 +	    (
   1.344 +	     Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.345 +	     Recon_Transfer.apply_res_thm reconstr goalstring;
   1.346 +	     Pretty.writeln(Pretty.str  (oct_char "361"));
   1.347 +	     
   1.348 +	     goals_being_watched := ((!goals_being_watched) - 1);
   1.349 +     
   1.350 +	     if ((!goals_being_watched) = 0)
   1.351 +	     then 
   1.352 +		(let val _ = File.write (File.tmp_path (Path.basic "foo_reap_found"))
   1.353 +		     ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n")
   1.354 +		 in
   1.355 +		     reapWatcher (childpid,childin, childout); ()
   1.356 +		 end)
   1.357 +	     else ()
   1.358 +	    )
   1.359 +	    (* if there's no proof, but a message from Spass *)
   1.360 +	    else if ((substring (reconstr, 0,5))= "SPASS")
   1.361 +		 then
   1.362 +		    (goals_being_watched := (!goals_being_watched) -1;
   1.363 +		     Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.364 +		      Pretty.writeln(Pretty.str (goalstring^reconstr));
   1.365 +		      Pretty.writeln(Pretty.str  (oct_char "361"));
   1.366 +		      if (!goals_being_watched = 0)
   1.367 +		      then 
   1.368 +			  (File.write (File.tmp_path (Path.basic "foo_reap_comp"))
   1.369 +			       ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n");
   1.370 +			   reapWatcher (childpid,childin, childout); ())
   1.371 +		      else
   1.372 +			 ()
   1.373 +		)
   1.374 +		  (* if proof translation failed *)
   1.375 +		  else if ((substring (reconstr, 0,5)) = "Proof")
   1.376 +		  then 
   1.377 +		     (goals_being_watched := (!goals_being_watched) -1;
   1.378 +		      Pretty.writeln(Pretty.str ( (concat[(oct_char "360"), (oct_char "377")])));
   1.379 +		       Pretty.writeln(Pretty.str (goalstring^reconstr));
   1.380 +		       Pretty.writeln(Pretty.str  (oct_char "361"));
   1.381 +		       if (!goals_being_watched = 0)
   1.382 +		       then 
   1.383 +			  (File.write(File.tmp_path (Path.basic "foo_reap_comp"))
   1.384 +			      ("Reaping a watcher, goals watched is: "^(string_of_int (!goals_being_watched))^"\n");
   1.385 +			   reapWatcher (childpid,childin, childout); ())		       
   1.386 +		       else ())
   1.387 +	 	  else () (* add something here ?*)
   1.388 +	     end)
   1.389  
   1.390  
   1.391 -                                                                else  (* add something here ?*)
   1.392 -                                                                   ()
   1.393 -                                                             
   1.394 -                                       end)
   1.395 -
   1.396 +   
   1.397 +  in IsaSignal.signal (IsaSignal.usr1, IsaSignal.SIG_HANDLE vampire_proofHandler);
   1.398 +     IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE spass_proofHandler);
   1.399 +     (childin, childout, childpid)
   1.400  
   1.401 -                        
   1.402 -                       in IsaSignal.signal (IsaSignal.usr1, IsaSignal.SIG_HANDLE vampire_proofHandler);
   1.403 -                          IsaSignal.signal (IsaSignal.usr2, IsaSignal.SIG_HANDLE spass_proofHandler);
   1.404 -                          (childin, childout, childpid)
   1.405 -
   1.406 -                       end
   1.407 +  end
   1.408  
   1.409  
   1.410