# HG changeset patch
# User boehmes
# Date 1251100190 -7200
# Node ID 1899b8c47961c864e2369e20f475d28a05e66df0
# Parent  e756600502ccc2f45e8b42cbacdb078bf3c80ce9
more quoting for shell variables, canonical isabelle process

diff -r e756600502cc -r 1899b8c47961 src/HOL/Tools/Mirabelle/lib/Tools/mirabelle
--- a/src/HOL/Tools/Mirabelle/lib/Tools/mirabelle	Mon Aug 24 08:50:29 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/lib/Tools/mirabelle	Mon Aug 24 09:49:50 2009 +0200
@@ -7,15 +7,17 @@
 
 PRG="$(basename "$0")"
 
-function action_names() {
+function print_action_names() {
   TOOLS="$MIRABELLE_HOME/Tools/mirabelle_*.ML"
-  ACTION_NAMES=`find $TOOLS | sed 's/.*mirabelle_\(.*\)\.ML/\1/'`
+  for NAME in $TOOLS
+  do
+    echo $NAME | sed 's/.*mirabelle_\(.*\)\.ML/    \1/'
+  done
 }
 
 function usage() {
   out="$MIRABELLE_OUTPUT_PATH"
   timeout="$MIRABELLE_TIMEOUT"
-  action_names
   echo
   echo "Usage: isabelle $PRG [OPTIONS] ACTIONS FILES"
   echo
@@ -31,14 +33,11 @@
   echo
   echo "  ACTIONS is a colon-separated list of actions, where each action is"
   echo "  either NAME or NAME[KEY=VALUE,...,KEY=VALUE]. Available actions are:"
-  for NAME in $ACTION_NAMES
-  do
-    echo "    $NAME"
-  done
+  print_action_names
   echo
-  echo "  FILES is a space-separated list of theory files, where each file is"
-  echo "  either NAME.thy or NAME.thy[START:END] and START and END are numbers"
-  echo "  indicating the range the given actions are to be applied."
+  echo "  FILES is a list of theory files, where each file is either NAME.thy"
+  echo "  or NAME.thy[START:END] and START and END are numbers indicating the"
+  echo "  range the given actions are to be applied."
   echo
   exit 1
 }
@@ -48,7 +47,7 @@
 
 # options
 
-while getopts "L:T:O:vt:" OPT
+while getopts "L:T:O:vt:?" OPT
 do
   case "$OPT" in
     L)
@@ -61,7 +60,7 @@
       MIRABELLE_OUTPUT_PATH="$OPTARG"
       ;;
     v)
-      MIRABELLE_VERBOSE=true
+      MIRABELLE_VERBOSE="true"
       ;;
     t)
       MIRABELLE_TIMEOUT="$OPTARG"
@@ -81,13 +80,13 @@
 
 # setup
 
-mkdir -p $MIRABELLE_OUTPUT_PATH
+mkdir -p "$MIRABELLE_OUTPUT_PATH"
 
 
 ## main
 
 for FILE in "$@"
 do
-  perl -w $MIRABELLE_HOME/lib/scripts/mirabelle.pl $ACTIONS "$FILE"
+  perl -w "$MIRABELLE_HOME/lib/scripts/mirabelle.pl" "$ACTIONS" "$FILE"
 done
 
diff -r e756600502cc -r 1899b8c47961 src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl
--- a/src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl	Mon Aug 24 08:50:29 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl	Mon Aug 24 09:49:50 2009 +0200
@@ -125,7 +125,7 @@
 print LOG_FILE "\n\n";
 close(LOG_FILE);
 
-my $r = system "$isabelle_home/bin/isabelle-process " .
+my $r = system "\"$ISABELLE_PROCESS\" " .
   "-e 'use \"$root_file\";' -q $mirabelle_logic" . "\n";