# HG changeset patch
# User desharna
# Date 1642583484 -3600
# Node ID 877f0c44d77e26e21a6afab232aba73d36b4654d
# Parent  fc664e4fbf6da5ad7aa7596826233338ab3e4111
added cpu time (in ms) to Mirabelle run_action output

diff -r fc664e4fbf6d -r 877f0c44d77e src/HOL/Tools/Mirabelle/mirabelle.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle.ML	Tue Jan 18 17:55:20 2022 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML	Wed Jan 19 10:11:24 2022 +0100
@@ -135,10 +135,10 @@
     val goal_name_path = Path.basic (#name command)
     val line_path = Path.basic (string_of_int (the (Position.line_of pos)));
     val offset_path = Path.basic (string_of_int (the (Position.offset_of pos)));
+    val ({cpu, ...}, s) = Timing.timing run_action_function (fn () => run_action command);
     val export_name =
       Path.binding0 (Path.basic "mirabelle" + action_path + Path.basic "goal" + goal_name_path +
-        line_path + offset_path);
-    val s = run_action_function (fn () => run_action command);
+        line_path + offset_path + Path.basic (string_of_int (Time.toMilliseconds cpu)));
   in
     if s <> "" then
       Export.export thy export_name [XML.Text s]
diff -r fc664e4fbf6d -r 877f0c44d77e src/HOL/Tools/Mirabelle/mirabelle.scala
--- a/src/HOL/Tools/Mirabelle/mirabelle.scala	Tue Jan 18 17:55:20 2022 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle.scala	Wed Jan 19 10:11:24 2022 +0100
@@ -87,9 +87,9 @@
                     Export.explode_name(args.name) match {
                       case List("mirabelle", action, "initialize") => action + " initialize "
                       case List("mirabelle", action, "finalize") => action + " finalize   "
-                      case List("mirabelle", action, "goal", goal_name, line, offset) =>
-                        action + " goal." + String.format("%-5s", goal_name) + " " + args.theory_name + " " +
-                          line + ":" + offset + "  "
+                      case List("mirabelle", action, "goal", goal_name, line, offset, cpu_ms) =>
+                        action + " goal." + String.format("%-5s", goal_name) + " " + String.format("%5sms", cpu_ms) + " " +
+                          args.theory_name + " " + line + ":" + offset + "  "
                       case _ => ""
                     }
                   val body = Library.prefix_lines(prefix, lines) + "\n"