# HG changeset patch
# User boehmes
# Date 1252158412 -7200
# Node ID 1b70db55c81145c51522f8be8c3d38d46c1af04d
# Parent  f20cc66b2c7412e99da6def580fe8cadb51271db
Mirabelle: command-line action options may either be key=value or just key

diff -r f20cc66b2c74 -r 1b70db55c811 src/HOL/Mirabelle/doc/options.txt
--- a/src/HOL/Mirabelle/doc/options.txt	Sat Sep 05 11:45:57 2009 +0200
+++ b/src/HOL/Mirabelle/doc/options.txt	Sat Sep 05 15:46:52 2009 +0200
@@ -2,6 +2,5 @@
 
   * prover=NAME: name of the external prover to call
   * keep=PATH: path where to keep temporary files created by sledgehammer 
-  * metis=X: apply metis with the theorems found by sledgehammer (X may be any
-      non-empty string)
-  * full_types=X: turn on full-typed encoding (X may be any non-empty string)
+  * metis: apply metis with the theorems found by sledgehammer
+  * full_types: turn on full-typed encoding
diff -r f20cc66b2c74 -r 1b70db55c811 src/HOL/Mirabelle/lib/Tools/mirabelle
--- a/src/HOL/Mirabelle/lib/Tools/mirabelle	Sat Sep 05 11:45:57 2009 +0200
+++ b/src/HOL/Mirabelle/lib/Tools/mirabelle	Sat Sep 05 15:46:52 2009 +0200
@@ -32,9 +32,12 @@
   echo "  at all proof steps in the given theory files."
   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:"
+  echo "  either NAME or NAME[OPTION,...,OPTION]. Available actions are:"
   print_action_names
   echo
+  echo "  A list of available OPTIONs can be found here:"
+  echo "    $MIRABELLE_HOME/doc/options.txt"
+  echo
   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."
diff -r f20cc66b2c74 -r 1b70db55c811 src/HOL/Mirabelle/lib/scripts/mirabelle.pl
--- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Sat Sep 05 11:45:57 2009 +0200
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl	Sat Sep 05 15:46:52 2009 +0200
@@ -82,6 +82,10 @@
         print SETUP_FILE "$sep(\"$1\", \"$2\")";
         $sep = ", ";
       }
+      elsif (m/\s*(.*)\s*/) {
+	print SETUP_FILE "$sep(\"$1\", \"\")";
+	$sep = ", ";
+      }
     }
     print SETUP_FILE "] *}\n";
   }