# HG changeset patch
# User wenzelm
# Date 1300031579 -3600
# Node ID f9a2e10c49cb53e022d4ce828eeac8805d73804a
# Parent  30732d2390c8e11466c9fe058dbb8b1c20bfcb27
more conventional Mutabelle settings -- similar to Mirabelle;

diff -r 30732d2390c8 -r f9a2e10c49cb src/HOL/Mutabelle/etc/settings
--- a/src/HOL/Mutabelle/etc/settings	Sun Mar 13 16:38:54 2011 +0100
+++ b/src/HOL/Mutabelle/etc/settings	Sun Mar 13 16:52:59 2011 +0100
@@ -2,8 +2,8 @@
 
 MUTABELLE_HOME="$COMPONENT"
 
-DEFAULT_MUTABELLE_LOGIC=HOL
-DEFAULT_MUTABELLE_IMPORT_THEORY=Complex_Main
-DEFAULT_MUTABELLE_OUTPUT_PATH=/tmp/mutabelle
+MUTABELLE_LOGIC=HOL
+MUTABELLE_IMPORT_THEORY=Complex_Main
+MUTABELLE_OUTPUT_PATH=/tmp/mutabelle
 
 ISABELLE_TOOLS="$ISABELLE_TOOLS:$MUTABELLE_HOME/lib/Tools"
diff -r 30732d2390c8 -r f9a2e10c49cb src/HOL/Mutabelle/lib/Tools/mutabelle
--- a/src/HOL/Mutabelle/lib/Tools/mutabelle	Sun Mar 13 16:38:54 2011 +0100
+++ b/src/HOL/Mutabelle/lib/Tools/mutabelle	Sun Mar 13 16:52:59 2011 +0100
@@ -12,9 +12,9 @@
   echo "Usage: isabelle $PRG [OPTIONS] THEORY"
   echo
   echo "  Options are:"
-  echo "    -L LOGIC     parent logic to use (default $DEFAULT_MUTABELLE_LOGIC)"
-  echo "    -T THEORY    parent theory to use (default $DEFAULT_MUTABELLE_IMPORT_THEORY)"
-  echo "    -O DIR       output directory for test data (default $DEFAULT_MUTABELLE_OUTPUT_PATH)"
+  echo "    -L LOGIC     parent logic to use (default $MUTABELLE_LOGIC)"
+  echo "    -T THEORY    parent theory to use (default $MUTABELLE_IMPORT_THEORY)"
+  echo "    -O DIR       output directory for test data (default $MUTABELLE_OUTPUT_PATH)"
   echo
   echo "  THEORY is the name of the theory of which all theorems should be"
   echo "  mutated and tested."
@@ -27,10 +27,7 @@
 
 # options
 
-MUTABELLE_LOGIC="$DEFAULT_MUTABELLE_LOGIC"
-MUTABELLE_OUTPUT_PATH="$DEFAULT_MUTABELLE_OUTPUT_PATH"
-
-MUTABELLE_IMPORT_THEORY=""
+MUTABELLE_IMPORTS=""
 
 while getopts "L:T:O:" OPT
 do
@@ -39,7 +36,7 @@
       MUTABELLE_LOGIC="$OPTARG"
       ;;
     T)
-      MUTABELLE_IMPORT_THEORY="$MUTABELLE_IMPORT_THEORY \"$OPTARG\""
+      MUTABELLE_IMPORTS="$MUTABELLE_IMPORTS \"$OPTARG\""
       ;;
     O)      
       MUTABELLE_OUTPUT_PATH="$OPTARG"
@@ -52,9 +49,9 @@
 
 shift $(($OPTIND - 1))
 
-if [ "$MUTABELLE_IMPORT_THEORY" = "" ]
+if [ "$MUTABELLE_IMPORTS" = "" ]
 then
-  MUTABELLE_IMPORT_THEORY="$DEFAULT_MUTABELLE_IMPORT_THEORY"
+  MUTABELLE_IMPORTS="$MUTABELLE_IMPORT_THEORY"
 fi
 
 [ "$#" -ne 1 ] && usage
@@ -63,16 +60,18 @@
 
 export MUTABELLE_OUTPUT_PATH
 
+
 ## main
 
 echo "Starting Mutabelle..."
 
+
 # setup
 
 mkdir -p "$MUTABELLE_OUTPUT_PATH"
 
 echo "theory Mutabelle_Test
-imports $MUTABELLE_IMPORT_THEORY
+imports $MUTABELLE_IMPORTS
 uses     
   \"$MUTABELLE_HOME/mutabelle.ML\"
   \"$MUTABELLE_HOME/mutabelle_extra.ML\"
@@ -100,13 +99,15 @@
 
 end" > "$MUTABELLE_OUTPUT_PATH/Mutabelle_Test.thy"
 
+
 # execution
 
-"$ISABELLE_PROCESS" -e 'use_thy "$MUTABELLE_OUTPUT_PATH/Mutabelle_Test"' -q $MUTABELLE_LOGIC > /dev/null 2>&1
+"$ISABELLE_PROCESS" -e 'use_thy "$MUTABELLE_OUTPUT_PATH/Mutabelle_Test"' -q "$MUTABELLE_LOGIC" > /dev/null 2>&1
 
 
 [ $? -ne 0 ] && echo "isabelle processing of mutabelle failed"
 
+
 # make statistics
 
 function count() {