--- a/src/HOL/Mirabelle/lib/Tools/mirabelle Fri Sep 04 13:57:56 2009 +0200
+++ b/src/HOL/Mirabelle/lib/Tools/mirabelle Sat Sep 05 11:45:57 2009 +0200
@@ -26,6 +26,7 @@
echo " -T THEORY parent theory to use (default $MIRABELLE_THEORY)"
echo " -O DIR output directory for test data (default $out)"
echo " -t TIMEOUT timeout for each action in seconds (default $timeout)"
+ echo " -q be quiet (suppress output of Isabelle process)"
echo
echo " Apply the given actions (i.e., automated proof tools)"
echo " at all proof steps in the given theory files."
@@ -46,7 +47,7 @@
# options
-while getopts "L:T:O:t:?" OPT
+while getopts "L:T:O:t:q?" OPT
do
case "$OPT" in
L)
@@ -61,15 +62,20 @@
t)
MIRABELLE_TIMEOUT="$OPTARG"
;;
+ q)
+ MIRABELLE_QUIET="true"
+ ;;
\?)
usage
;;
esac
done
+export MIRABELLE_QUIET
+
shift $(($OPTIND - 1))
-ACTIONS="$1"
+export MIRABELLE_ACTIONS="$1"
shift
@@ -83,6 +89,6 @@
for FILE in "$@"
do
- perl -w "$MIRABELLE_HOME/lib/scripts/mirabelle.pl" "$ACTIONS" "$FILE"
+ perl -w "$MIRABELLE_HOME/lib/scripts/mirabelle.pl" "$FILE"
done