--- a/src/HOL/Mirabelle/lib/Tools/mirabelle Tue Mar 06 17:01:37 2012 +0000
+++ b/src/HOL/Mirabelle/lib/Tools/mirabelle Wed Mar 07 13:00:30 2012 +0000
@@ -26,7 +26,7 @@
echo " -T THEORY parent theory to use (default $MIRABELLE_THEORY)"
echo " -O DIR output directory for test data (default $out)"
echo " -t TIMEOUT timeout for each action in seconds (default $timeout)"
- echo " -q be quiet (suppress output of Isabelle process)"
+ echo " -q be quiet (suppress output of Isabelle process)"
echo
echo " Apply the given actions (i.e., automated proof tools)"
echo " at all proof steps in the given theory files."
--- a/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Tue Mar 06 17:01:37 2012 +0000
+++ b/src/HOL/Mirabelle/lib/scripts/mirabelle.pl Wed Mar 07 13:00:30 2012 +0000
@@ -67,7 +67,7 @@
$tools
begin
-setup {*
+setup {*
Config.put_global Mirabelle.logfile "$log_file" #>
Config.put_global Mirabelle.timeout $timeout #>
Config.put_global Mirabelle.start_line $start_line #>
@@ -76,7 +76,9 @@
END
-foreach (reverse(split(/:/, $actions))) {
+@action_list = split(/:/, $actions);
+
+foreach (reverse(@action_list)) {
if (m/([^[]*)(?:\[(.*)\])?/) {
my ($name, $settings_str) = ($1, $2 || "");
$name =~ s/^([a-z])/\U$1/;
@@ -88,8 +90,8 @@
$sep = ", ";
}
elsif (m/\s*(.*)\s*/) {
- print SETUP_FILE "$sep(\"$1\", \"\")";
- $sep = ", ";
+ print SETUP_FILE "$sep(\"$1\", \"\")";
+ $sep = ", ";
}
}
print SETUP_FILE "] *}\n";
@@ -121,8 +123,8 @@
open(LOG_FILE, ">$log_file");
print LOG_FILE "Run of $new_thy_file with:\n";
-foreach $name (@action_names) {
- print LOG_FILE " $name\n";
+foreach $action (@action_list) {
+ print LOG_FILE " $action\n";
}
close(LOG_FILE);