diff -r b389f108c485 -r 028059faa963 src/HOL/Tools/ATP/VampireCommunication.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/ATP/VampireCommunication.ML	Thu Mar 31 19:29:26 2005 +0200
@@ -0,0 +1,117 @@
+(*  Title:      VampireCommunication.ml
+    Author:     Claire Quigley
+    Copyright   2004  University of Cambridge
+*)
+
+(***************************************************************************)
+(*  Code to deal with the transfer of proofs from a Vampire process        *)
+(***************************************************************************)
+
+(***********************************)
+(*  Write vampire output to a file *)
+(***********************************)
+
+fun logVampInput (instr, fd) = let val thisLine = TextIO.inputLine instr 
+			 in if thisLine = "%==============  End of proof. ==================\n" 
+			    then TextIO.output (fd, thisLine)
+      			  else (
+				TextIO.output (fd, thisLine); logVampInput (instr,fd))
+ 			 end;
+
+(**********************************************************************)
+(*  Transfer the vampire output from the watcher to the input pipe of *)
+(*  the main Isabelle process                                         *)
+(**********************************************************************)
+
+fun transferVampInput (fromChild, toParent, ppid) = let 
+                         val thisLine = TextIO.inputLine fromChild 
+			 in 
+                            if (thisLine = "%==============  End of proof. ==================\n" )
+			    then ( 
+                                   TextIO.output (toParent, thisLine);
+                                   TextIO.flushOut toParent
+                                  )
+      			    else (
+				TextIO.output (toParent, thisLine); 
+                                TextIO.flushOut toParent;
+                                transferVampInput (fromChild, toParent, ppid)
+                                )
+ 			 end;
+
+
+(*********************************************************************************)
+(*  Inspect the output of a vampire process to see if it has found a proof,      *)
+(*  and if so, transfer output to the input pipe of the main Isabelle process    *)
+(*********************************************************************************)
+
+fun startVampireTransfer (fromChild, toParent, ppid, childCmd) = 
+                                       if (isSome (TextIO.canInput(fromChild, 5)))
+                                       then
+                                       (
+                                       let val thisLine = TextIO.inputLine fromChild  
+                                           in                 
+                                             if (thisLine = "% Proof found. Thanks to Tanya!\n" )
+                                             then      
+                                              ( 
+                                                Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr1);
+                                                TextIO.output (toParent,childCmd^"\n" );
+                                                TextIO.flushOut toParent;
+                                                TextIO.output (toParent, thisLine);
+                                                TextIO.flushOut toParent;
+
+                                                transferVampInput (fromChild, toParent, ppid);
+                                                true)
+                                              else if (thisLine = "% Unprovable.\n" ) 
+                                                   then 
+                                                       (
+                                                        Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr1);
+                                                        TextIO.output (toParent,childCmd^"\n" );
+                                                        TextIO.flushOut toParent;
+                                                        TextIO.output (toParent, thisLine);
+                                                        TextIO.flushOut toParent;
+
+                                                        true)
+                                                   else if (thisLine = "% Proof not found.\n")
+                                                        then 
+                                                            (Posix.Process.kill(Posix.Process.K_PROC ppid, Posix.Signal.usr1);                                                            TextIO.output (toParent,childCmd^"\n" );
+                                                             TextIO.flushOut toParent;
+                                                             TextIO.output (toParent, thisLine);
+                                                             TextIO.flushOut toParent;
+                                                             true)
+                                                        else 
+                                                           (
+                                                             startVampireTransfer (fromChild, toParent, ppid, childCmd)
+                                                            )
+                                            end
+                                           )
+                                         else (false)
+
+
+(***********************************************************************)
+(*  Function used by the Isabelle process to read in a vampire proof   *)
+(***********************************************************************)
+
+fun getVampInput instr = let val thisLine = TextIO.inputLine instr 
+			 in 
+                           if (thisLine = "%==============  End of proof. ==================\n" )
+			    then
+                               (
+                                (Pretty.writeln(Pretty.str  (concat["vampire",thisLine])));()
+                               )
+                             else if (thisLine = "% Unprovable.\n" ) 
+                                  then 
+                                     (
+                                      (Pretty.writeln(Pretty.str (concat["vampire",thisLine])));()
+                                      )
+                                   else if (thisLine = "% Proof not found.\n")
+                                        then 
+                                            (
+                                             Pretty.writeln(Pretty.str (concat["vampire", thisLine]));()
+                                             )
+
+
+                                         else 
+                                            (
+				              Pretty.writeln(Pretty.str (concat["vampire",thisLine])); getVampInput instr
+                                             )
+ 			 end;