diff -r 2463cba9f18f -r f54c32c413a9 src/HOL/Mirabelle/lib/Tools/mirabelle --- a/src/HOL/Mirabelle/lib/Tools/mirabelle Tue Jun 20 21:41:59 2017 +0200 +++ b/src/HOL/Mirabelle/lib/Tools/mirabelle Wed Jun 21 22:48:55 2017 +0200 @@ -28,11 +28,12 @@ echo echo " Options are:" echo " -L LOGIC parent logic to use (default $MIRABELLE_LOGIC)" + echo " -O DIR output directory for test data (default $out)" + echo " -S FILE user-provided setup file (no actions required)" echo " -T THEORY parent theory to use (default $MIRABELLE_THEORY)" - echo " -O DIR output directory for test data (default $out)" + echo " -d DIR include session directory" + echo " -q be quiet (suppress output of Isabelle process)" echo " -t TIMEOUT timeout for each action in seconds (default $timeout)" - echo " -q be quiet (suppress output of Isabelle process)" - echo " -S FILE user-provided setup file (no actions required)" echo echo " Apply the given actions (i.e., automated proof tools)" echo " at all proof steps in the given theory files." @@ -64,9 +65,10 @@ [ $# -eq 0 ] && usage +MIRABELLE_DIR= MIRABELLE_SETUP_FILE= -while getopts "L:T:O:t:S:q?" OPT +while getopts "L:T:O:d:t:S:q?" OPT do case "$OPT" in L) @@ -78,6 +80,9 @@ O) MIRABELLE_OUTPUT_PATH="$OPTARG" ;; + d) + MIRABELLE_DIR="$OPTARG" + ;; t) MIRABELLE_TIMEOUT="$OPTARG" ;; @@ -93,6 +98,7 @@ esac done +export MIRABELLE_DIR export MIRABELLE_SETUP_FILE export MIRABELLE_QUIET