# HG changeset patch
# User krauss
# Date 1300868149 -3600
# Node ID 6a147393c62a65a2a6551b0fd1c650bb10622c4e
# Parent  b579e787b582e91745529698baed2f7d17681a62
replace hardwired MIRABELLE_OUTPUT_PATH by temporary directory derived from ISABELLE_TMP_PREFIX and $$ -- old behaviour can be achieved by manually setting MIRABELLE_OUTPUT_PATH

diff -r b579e787b582 -r 6a147393c62a src/HOL/Mirabelle/etc/settings
--- a/src/HOL/Mirabelle/etc/settings	Tue Mar 22 21:22:50 2011 +0100
+++ b/src/HOL/Mirabelle/etc/settings	Wed Mar 23 09:15:49 2011 +0100
@@ -4,7 +4,6 @@
 
 MIRABELLE_LOGIC=HOL
 MIRABELLE_THEORY=Main
-MIRABELLE_OUTPUT_PATH=/tmp/mirabelle
 MIRABELLE_TIMEOUT=30
 
 ISABELLE_TOOLS="$ISABELLE_TOOLS:$MIRABELLE_HOME/lib/Tools"
diff -r b579e787b582 -r 6a147393c62a src/HOL/Mirabelle/lib/Tools/mirabelle
--- a/src/HOL/Mirabelle/lib/Tools/mirabelle	Tue Mar 22 21:22:50 2011 +0100
+++ b/src/HOL/Mirabelle/lib/Tools/mirabelle	Wed Mar 23 09:15:49 2011 +0100
@@ -16,7 +16,7 @@
 }
 
 function usage() {
-  out="$MIRABELLE_OUTPUT_PATH"
+  [ -n "$MIRABELLE_OUTPUT_PATH" ] && out="$MIRABELLE_OUTPUT_PATH" || out="None"
   timeout="$MIRABELLE_TIMEOUT"
   echo
   echo "Usage: isabelle $PRG [OPTIONS] ACTIONS FILES"
@@ -102,8 +102,14 @@
 
 # setup
 
+if [ -z "$MIRABELLE_OUTPUT_PATH" ]; then
+  MIRABELLE_OUTPUT_PATH="${ISABELLE_TMP_PREFIX}-mirabelle$$"
+  PURGE_OUTPUT="true"
+fi
+
 mkdir -p "$MIRABELLE_OUTPUT_PATH"
 
+export MIRABELLE_OUTPUT_PATH
 
 ## main
 
@@ -112,3 +118,9 @@
   perl -w "$MIRABELLE_HOME/lib/scripts/mirabelle.pl" "$FILE" || fail "Mirabelle failed."
 done
 
+
+## cleanup
+
+if [ -n "$PURGE_OUTPUT" ]; then
+  rm -rf "$MIRABELLE_OUTPUT_PATH"
+fi