# HG changeset patch
# User wenzelm
# Date 1645123230 -3600
# Node ID f700ca53e3aead910b0d5f0e2ad65440363b502f
# Parent  d76b150efdc278624aabad98e820a8a6c5bae56a# Parent  35a5c4b16024bc22808d883a1799c7ebd8741165
merged

diff -r 35a5c4b16024 -r f700ca53e3ae NEWS
--- a/NEWS	Thu Feb 17 19:00:14 2022 +0100
+++ b/NEWS	Thu Feb 17 19:40:30 2022 +0100
@@ -57,10 +57,11 @@
   - Replaced sledgehammer option "keep" by
     "keep_probs", for problems files, and
     "keep_proofs" for proof files. Minor INCOMPATIBILITY.
-  - Added option "-r INT" to randomize the goals with a given seed before
+  - Added option "-r INT" to randomize the goals with a given 64-bit seed before
     selection.
   - Added option "-y" for a dry run.
   - Renamed run_action to run in Mirabelle.action record. Minor INCOMPATIBILITY.
+  - Run the actions on goals before commands "unfolding" and "using".
 
 * Meson
   - Added support for polymorphic "using" facts. Minor INCOMPATIBILITY.
diff -r 35a5c4b16024 -r f700ca53e3ae src/HOL/Tools/Mirabelle/mirabelle.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle.ML	Thu Feb 17 19:00:14 2022 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML	Thu Feb 17 19:40:30 2022 +0100
@@ -187,7 +187,7 @@
 
 (* presentation hook *)
 
-val whitelist = ["apply", "by", "proof"];
+val whitelist = ["apply", "by", "proof", "unfolding", "using"];
 
 val _ =
   Build.add_hook (fn qualifier => fn loaded_theories =>
diff -r 35a5c4b16024 -r f700ca53e3ae src/HOL/Tools/Mirabelle/mirabelle.scala
--- a/src/HOL/Tools/Mirabelle/mirabelle.scala	Thu Feb 17 19:00:14 2022 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle.scala	Thu Feb 17 19:40:30 2022 +0100
@@ -88,7 +88,7 @@
                       case List("mirabelle", action, "initialize") => action + " initialize "
                       case List("mirabelle", action, "finalize") => action + " finalize   "
                       case List("mirabelle", action, "goal", goal_name, line, offset, cpu_ms) =>
-                        action + " goal." + String.format("%-5s", goal_name) + " " + String.format("%5sms", cpu_ms) + " " +
+                        action + " goal." + String.format("%-9s", goal_name) + " " + String.format("%5sms", cpu_ms) + " " +
                           args.theory_name + " " + line + ":" + offset + "  "
                       case _ => ""
                     }