# 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"; }