# HG changeset patch
# User blanchet
# Date 1498078135 -7200
# Node ID f54c32c413a9a6f31dd5e34db97b60f3e12abdaf
# Parent  2463cba9f18f0b82a6daa9adf5adc0550a339238
added -d option to Mirabelle

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
 
diff -r 2463cba9f18f -r f54c32c413a9 src/HOL/Mirabelle/lib/scripts/mirabelle.pl
--- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Tue Jun 20 21:41:59 2017 +0200
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Wed Jun 21 22:48:55 2017 +0200
@@ -10,6 +10,7 @@
 
 my $isabelle_home = $ENV{'ISABELLE_HOME'};
 my $mirabelle_home = $ENV{'MIRABELLE_HOME'};
+my $mirabelle_dir = $ENV{'MIRABELLE_DIR'};
 my $mirabelle_logic = $ENV{'MIRABELLE_LOGIC'};
 my $mirabelle_theory = $ENV{'MIRABELLE_THEORY'};
 my $output_path = $ENV{'MIRABELLE_OUTPUT_PATH'};
@@ -160,7 +161,9 @@
 
 my $cmd =
   "isabelle process -o quick_and_dirty -o threads=1" .
-  " -T \"$path/$new_thy_name\" -l $mirabelle_logic" . $quiet;
+  " -T \"$path/$new_thy_name\" " .
+  ($mirabelle_dir ? "-d " . $mirabelle_dir . " " : "") .
+  "-l $mirabelle_logic" . $quiet;
 my $result = system "bash", "-c", $cmd;
 
 if ($output_log) {