# HG changeset patch
# User blanchet
# Date 1280334915 -7200
# Node ID ef45bcccc9fdc6f85d02cc0b328dafd64d280dbf
# Parent  3b80d6082131182ae3e95e203a3e9d1cb64a7163
remove needless "-x" option, now that (1) we can't handle remote SPASS anymore; and (2) we can a priori parse the SPASS syntax in "Sledgehammer_Proof_Reconstruct" anyway

diff -r 3b80d6082131 -r ef45bcccc9fd src/HOL/Tools/ATP_Manager/scripts/remote_atp
--- a/src/HOL/Tools/ATP_Manager/scripts/remote_atp	Wed Jul 28 18:32:54 2010 +0200
+++ b/src/HOL/Tools/ATP_Manager/scripts/remote_atp	Wed Jul 28 18:35:15 2010 +0200
@@ -24,7 +24,7 @@
 
 #----Get format and transform options if specified
 my %Options;
-getopts("hwxs:t:c:",\%Options);
+getopts("hws:t:c:",\%Options);
 
 #----Usage
 sub usage() {
@@ -32,7 +32,6 @@
   print("    <options> are ...\n");
   print("    -h            - print this help\n");
   print("    -w            - list available ATP systems\n");
-  print("    -x            - use X2TPTP to convert output of prover\n");
   print("    -s<system>    - specified system to use\n");
   print("    -t<timelimit> - CPU time limit for system\n");
   print("    -c<command>   - custom command for system\n");
@@ -104,39 +103,7 @@
 } elsif ($Response->content =~ /WARNING: (\S*) does not exist/) {
   print "Specified System $1 does not exist\n";
   exit(-1);
-} elsif (exists($Options{'x'}) &&
-  $Response->content =~
-    /%\s*Result\s*:\s*(Unsatisfiable|Theorem).*\n%\s*Output\s*:\s*(CNF)?Refutation.*\n%/ &&
-  $Response->content !~ /ERROR: Could not form TPTP format derivation/ )
-{
-  # converted output: extract proof
-  my @lines = split( /\n/, $Response->content);
-  my $extract = "";
-  foreach my $line (@lines){
-      #ignore comments
-      if ($line !~ /^%/ && !($line eq "")) {
-          $extract .= "$line";
-      }
-  }
-  # insert newlines after ').'
-  $extract =~ s/\s//g;
-  $extract =~ s/\)\.cnf/\)\.\ncnf/g;
-
-  print "========== ~~/lib/scripts/SystemOnTPTP extracted proof: ==========\n";
-  # orientation for "sledgehammer_proof_reconstruct.ML"
-  print "# SZS output start CNFRefutation.\n";
-  print "$extract\n";
-  print "# SZS output end CNFRefutation.\n";
-  # can be useful for debugging; Isabelle ignores this
-  print "============== original response from SystemOnTPTP: ==============\n";
+} else {
   print $Response->content;
   exit(0);
-} elsif (!exists($Options{'x'})) {
-  # pass output directly to Isabelle
-  print $Response->content;
-  exit(0);
-}else {
-  print "Remote script could not extract proof:\n".$Response->content;
-  exit(-1);
 }
-