eliminated hardwired MUTABELLE_OUTPUT_PATH (cf. 6a147393c62a)
authorkrauss
Fri, 25 Mar 2011 21:38:41 +0100
changeset 42119 21714b0de625
parent 42118 a51761c262d1
child 42120 b8f176348f44
eliminated hardwired MUTABELLE_OUTPUT_PATH (cf. 6a147393c62a)
src/HOL/Mutabelle/etc/settings
src/HOL/Mutabelle/lib/Tools/mutabelle
--- a/src/HOL/Mutabelle/etc/settings	Fri Mar 25 17:09:21 2011 +0100
+++ b/src/HOL/Mutabelle/etc/settings	Fri Mar 25 21:38:41 2011 +0100
@@ -4,6 +4,5 @@
 
 MUTABELLE_LOGIC=HOL
 MUTABELLE_IMPORT_THEORY=Complex_Main
-MUTABELLE_OUTPUT_PATH=/tmp/mutabelle
 
 ISABELLE_TOOLS="$ISABELLE_TOOLS:$MUTABELLE_HOME/lib/Tools"
--- a/src/HOL/Mutabelle/lib/Tools/mutabelle	Fri Mar 25 17:09:21 2011 +0100
+++ b/src/HOL/Mutabelle/lib/Tools/mutabelle	Fri Mar 25 21:38:41 2011 +0100
@@ -8,6 +8,7 @@
 PRG="$(basename "$0")"
 
 function usage() {
+  [ -n "$MUTABELLE_OUTPUT_PATH" ] || MUTABELLE_OUTPUT_PATH="None"
   echo
   echo "Usage: isabelle $PRG [OPTIONS] THEORY"
   echo
@@ -58,6 +59,11 @@
 
 MUTABELLE_TEST_THEORY="$1"
 
+if [ -z "$MUTABELLE_OUTPUT_PATH" ]; then
+  MUTABELLE_OUTPUT_PATH="${ISABELLE_TMP_PREFIX}-mutabelle$$"
+  PURGE_OUTPUT="true"
+fi
+
 export MUTABELLE_OUTPUT_PATH
 
 
@@ -121,3 +127,9 @@
 echo "nitpick     : C: $(count "nitpick" "GenuineCex") N: $(count "nitpick" "NoCex") \
 T: $(count "nitpick" "Timeout") E: $(count "nitpick" "Error")"
 
+
+## cleanup
+
+if [ -n "$PURGE_OUTPUT" ]; then
+  rm -rf "$MUTABELLE_OUTPUT_PATH"
+fi