# HG changeset patch
# User blanchet
# Date 1328208118 -3600
# Node ID 3069344da6264e00e07d4c8bcd7d3c6782e38b8f
# Parent  ef8d65f64f777e8a8d8b55e2bcb2801d3926ea5a
improve SPASS scripts

diff -r ef8d65f64f77 -r 3069344da626 src/HOL/Tools/ATP/scripts/spass
--- a/src/HOL/Tools/ATP/scripts/spass	Thu Feb 02 15:14:18 2012 +0100
+++ b/src/HOL/Tools/ATP/scripts/spass	Thu Feb 02 19:41:58 2012 +0100
@@ -8,11 +8,11 @@
 options=${@:1:$(($#-1))}
 name=${@:$(($#)):1}
 
-"$SPASS_HOME/SPASS" -Flotter $name \
+"$SPASS_HOME/SPASS" -Flotter "$name" \
     | sed 's/description({$/description({*/' \
     | sed 's/set_ClauseFormulaRelation()\.//' \
     > $name.cnf
 cat $name.cnf
-"$SPASS_HOME/SPASS" $options $name.cnf \
+"$SPASS_HOME/SPASS" $options "$name.cnf" \
     | sed 's/\(Formulae used in the proof :\).*/\1 N\/A/'
-rm -f $name.cnf
+rm -f "$name.cnf"
diff -r ef8d65f64f77 -r 3069344da626 src/HOL/Tools/ATP/scripts/spass_new
--- a/src/HOL/Tools/ATP/scripts/spass_new	Thu Feb 02 15:14:18 2012 +0100
+++ b/src/HOL/Tools/ATP/scripts/spass_new	Thu Feb 02 19:41:58 2012 +0100
@@ -7,8 +7,11 @@
 options=${@:1:$(($#-1))}
 name=${@:$(($#)):1}
 
-rm -f $name.prf
-"$SPASS_NEW_HOME/SPASS" -FPDFGProof -FPFCR $options $name \
+rm -f "$name.prf"
+"$SPASS_NEW_HOME/SPASS" -FPDFGProof -FPFCR $options "$name" \
     | sed 's/\(Formulae used in the proof :\).*/\1 N\/A/'
-cat $name.prf
-#rm -f $name.cnf
+if [ -f "$name.prf" ]
+then
+  cat "$name.prf"
+  rm -f "$name.prf"
+fi