# HG changeset patch
# User desharna
# Date 1645017845 -3600
# Node ID 1dae5cbcd35874919231825b3ee09770e4512e9b
# Parent  8a48a9be91ce3157569020717f3ab62ae99de456
Mirabelle now considers goals preceding "unfolding" and "using" commands

diff -r 8a48a9be91ce -r 1dae5cbcd358 src/HOL/Tools/Mirabelle/mirabelle.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle.ML	Tue Feb 15 16:42:15 2022 +0000
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML	Wed Feb 16 14:24:05 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 8a48a9be91ce -r 1dae5cbcd358 src/HOL/Tools/Mirabelle/mirabelle.scala
--- a/src/HOL/Tools/Mirabelle/mirabelle.scala	Tue Feb 15 16:42:15 2022 +0000
+++ b/src/HOL/Tools/Mirabelle/mirabelle.scala	Wed Feb 16 14:24:05 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 _ => ""
                     }