# HG changeset patch
# User sultana
# Date 1331125230 0
# Node ID 1257c80988cd3e70f5402de0916424b1b419bb46
# Parent  57bf0cecb36609fe4b0e82870e8bf33520c605c7
added Mirabelle action info in its log file; tuned;

diff -r 57bf0cecb366 -r 1257c80988cd src/HOL/Mirabelle/lib/Tools/mirabelle
--- 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."
diff -r 57bf0cecb366 -r 1257c80988cd src/HOL/Mirabelle/lib/scripts/mirabelle.pl
--- 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);