# HG changeset patch
# User boehmes
# Date 1251096629 -7200
# Node ID e756600502ccc2f45e8b42cbacdb078bf3c80ce9
# Parent  9692b0714295d55a4d4073c7631a89a42bce864a
keep the modified (tested) theory,
added an explicit reference to the modified theory in the generated log file

diff -r 9692b0714295 -r e756600502cc src/HOL/Tools/Mirabelle/Tools/mirabelle.ML
--- a/src/HOL/Tools/Mirabelle/Tools/mirabelle.ML	Mon Aug 24 08:33:40 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle.ML	Mon Aug 24 08:50:29 2009 +0200
@@ -7,11 +7,11 @@
   type action
   val register : string * action -> theory -> theory
 
+  val logfile : string Config.T
   val timeout : int Config.T
   val verbose : bool Config.T
   val start_line : int Config.T
   val end_line : int Config.T
-  val set_logfile : string -> theory -> theory
 
   val goal_thm_of : Proof.state -> thm
   val can_apply : (Proof.context -> int -> tactic) -> Proof.state -> bool
@@ -59,10 +59,6 @@
 
 val setup = setup1 #> setup2 #> setup3 #> setup4 #> setup5
 
-fun set_logfile name =
-  let val _ = File.write (Path.explode name) ""   (* erase file content *)
-  in Config.put_thy logfile name end
-
 local
 
 fun log thy s =
@@ -90,15 +86,11 @@
   let val l = Config.get_thy thy start_line and r = Config.get_thy thy end_line
   in if in_range l r (Position.line_of pos) then f x else [] end
 
-fun pretty_print verbose pos name msgs =
+fun pretty_print pos name msgs =
   let
-    val file = the_default "unknown file" (Position.file_of pos)
-
     val str0 = string_of_int o the_default 0
     val loc = str0 (Position.line_of pos) ^ ":" ^ str0 (Position.column_of pos)
-
-    val full_loc = if verbose then file ^ ":" ^ loc else "at " ^ loc
-    val head = full_loc ^ " (" ^ name ^ "):"
+    val head = "at " ^ loc ^ " (" ^ name ^ "):"
 
     fun pretty_msg (name, msg) = Pretty.block (map Pretty.str [name, ": ", msg])
   in
@@ -119,7 +111,7 @@
     Actions.get thy
     |> Symtab.dest
     |> only_within_range thy pos (map_filter (apply_action (verb, secs) st))
-    |> (fn [] => () | msgs => log thy (pretty_print verb pos name msgs))
+    |> (fn [] => () | msgs => log thy (pretty_print pos name msgs))
   end
 
 end
diff -r 9692b0714295 -r e756600502cc src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl
--- a/src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl	Mon Aug 24 08:33:40 2009 +0200
+++ b/src/HOL/Tools/Mirabelle/lib/scripts/mirabelle.pl	Mon Aug 24 08:50:29 2009 +0200
@@ -43,9 +43,11 @@
 my $log_file = $output_path . "/" . $thy_name . ".log";
 
 my @action_files;
+my @action_names;
 foreach (split(/:/, $actions)) {
   if (m/([^[]*)/) {
     push @action_files, "\"$mirabelle_home/Tools/mirabelle_$1.ML\"";
+    push @action_names, $1;
   }
 }
 my $tools = "";
@@ -62,7 +64,7 @@
 begin
 
 setup {* 
-  Mirabelle.set_logfile "$log_file" #>
+  Config.put_thy Mirabelle.logfile "$log_file" #>
   Config.put_thy Mirabelle.timeout $timeout #>
   Config.put_thy Mirabelle.verbose $verbose #>
   Config.put_thy Mirabelle.start_line $start_line #>
@@ -115,6 +117,14 @@
 
 # run isabelle
 
+open(LOG_FILE, ">$log_file");
+print LOG_FILE "Run of $new_thy_file with:\n";
+foreach $name (@action_names) {
+  print LOG_FILE "  $name\n";
+}
+print LOG_FILE "\n\n";
+close(LOG_FILE);
+
 my $r = system "$isabelle_home/bin/isabelle-process " .
   "-e 'use \"$root_file\";' -q $mirabelle_logic" . "\n";
 
@@ -122,7 +132,6 @@
 # cleanup
 
 unlink $root_file;
-unlink $new_thy_file;
 unlink $setup_file;
 
 exit $r;