# 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