# HG changeset patch
# User paulson
# Date 1125667498 -7200
# Node ID aca2ce40be3575eda804ed77b9b0d016324be7e3
# Parent  19b460b39dad673f6a7cf37484580294d9ee1de0
deleted obsolete VampireCommunication.ML

diff -r 19b460b39dad -r aca2ce40be35 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Sep 02 09:50:58 2005 +0200
+++ b/src/HOL/IsaMakefile	Fri Sep 02 15:24:58 2005 +0200
@@ -92,7 +92,7 @@
   ROOT.ML Recdef.thy Reconstruction.thy Record.thy Refute.thy			\
   Relation.ML Relation.thy Relation_Power.thy Ring_and_Field.thy Set.ML		\
   Set.thy SetInterval.thy Sum_Type.thy Tools/ATP/SpassCommunication.ML		\
-  Tools/ATP/VampireCommunication.ML			\
+  Tools/ATP/VampCommunication.ML			\
   Tools/ATP/recon_order_clauses.ML Tools/ATP/recon_parse.ML			\
   Tools/ATP/recon_prelim.ML Tools/ATP/recon_transfer_proof.ML			\
   Tools/ATP/recon_translate_proof.ML Tools/ATP/res_clasimpset.ML		\
diff -r 19b460b39dad -r aca2ce40be35 src/HOL/Reconstruction.thy
--- a/src/HOL/Reconstruction.thy	Fri Sep 02 09:50:58 2005 +0200
+++ b/src/HOL/Reconstruction.thy	Fri Sep 02 15:24:58 2005 +0200
@@ -20,7 +20,6 @@
 	 "Tools/ATP/recon_parse.ML"
 	 "Tools/ATP/recon_transfer_proof.ML"
 	 "Tools/ATP/VampCommunication.ML"
-	 "Tools/ATP/VampireCommunication.ML"
 	 "Tools/ATP/SpassCommunication.ML"
 	 "Tools/ATP/watcher.sig"
 	 "Tools/ATP/watcher.ML"
diff -r 19b460b39dad -r aca2ce40be35 src/HOL/Tools/ATP/VampireCommunication.ML
--- a/src/HOL/Tools/ATP/VampireCommunication.ML	Fri Sep 02 09:50:58 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,114 +0,0 @@
-(*  Title:      VampireCommunication.ML
-    ID:         $Id$
-    Author:     Claire Quigley
-    Copyright   2004  University of Cambridge
-*)
-
-structure VampireCommunication =
-struct
-
-(***************************************************************************)
-(*  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;
-
-end;