# HG changeset patch
# User desharna
# Date 1632126656 -7200
# Node ID 6d111935299ca098b6cce9a9ea55a474d68d0547
# Parent  d97c48dc87fa4cf898b9427abe6a94eeec0ebc5d
produced Mirabelle output directly in ML until Scala output gets fixed

diff -r d97c48dc87fa -r 6d111935299c src/HOL/Tools/Mirabelle/mirabelle.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle.ML	Wed Oct 13 00:07:06 2021 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML	Mon Sep 20 10:30:56 2021 +0200
@@ -94,8 +94,10 @@
     if Exn.is_interrupt exn then Exn.reraise exn
     else print_exn exn;
 
-fun make_action_path ({index, label, name, ...} : action_context) =
-  Path.basic (if label = "" then string_of_int index ^ "." ^ name else label);
+fun make_action_string ({index, label, name, ...} : action_context) =
+  if label = "" then string_of_int index ^ "." ^ name else label;
+
+val make_action_path = Path.basic o make_action_string;
 
 fun finalize_action ({finalize, ...} : action) context =
   let
@@ -103,6 +105,8 @@
     val action_path = make_action_path context;
     val export_name =
       Path.binding0 (Path.basic "mirabelle" + action_path + Path.basic "finalize");
+    val () = File.append ((Path.dir (#output_dir context)) + Path.basic "mirabelle_ML.log")
+      (prefix_lines (make_action_string context ^ " finalize ") (YXML.content_of s) ^ "\n")
   in
     if s <> "" then
       Export.export \<^theory> export_name [XML.Text s]
@@ -121,6 +125,13 @@
       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);
+    val prefix = make_action_string context ^ " goal." ^ StringCvt.padRight #" " 6 (#name command) ^
+        Context.theory_long_name thy ^ " " ^
+        string_of_int (the (Position.line_of pos)) ^ ":" ^
+        string_of_int (the (Position.offset_of pos)) ^ " "
+    val _ = Substring.triml
+    val () = File.append ((Path.dir (#output_dir context)) + Path.basic "mirabelle_ML.log")
+      (prefix_lines prefix (YXML.content_of s) ^ "\n")
   in
     if s <> "" then
       Export.export thy export_name [XML.Text s]
@@ -189,7 +200,9 @@
           val mirabelle_stride = Options.default_int \<^system_option>\<open>mirabelle_stride\<close>;
           val mirabelle_max_calls = Options.default_int \<^system_option>\<open>mirabelle_max_calls\<close>;
           val mirabelle_theories = Options.default_string \<^system_option>\<open>mirabelle_theories\<close>;
-          val mirabelle_output_dir = Options.default_string \<^system_option>\<open>mirabelle_output_dir\<close>;
+          val mirabelle_output_dir = Options.default_string \<^system_option>\<open>mirabelle_output_dir\<close>
+            |> Path.explode
+            |> Isabelle_System.make_directory;
           val check_theory = check_theories (space_explode "," mirabelle_theories);
 
           fun make_commands (thy_index, (thy, segments)) =
@@ -219,9 +232,8 @@
           val contexts = actions |> map_index (fn (n, (label, name, args)) =>
             let
               val make_action = the (get_action name);
-              val action_subdir = if label = "" then string_of_int n ^ "." ^ name else label
-              val output_dir =
-                Path.append (Path.explode mirabelle_output_dir) (Path.basic action_subdir)
+              val action_subdir = if label = "" then string_of_int n ^ "." ^ name else label;
+              val output_dir = Path.append mirabelle_output_dir (Path.basic action_subdir);
               val context =
                 {index = n, label = label, name = name, arguments = args,
                  timeout = mirabelle_timeout, output_dir = output_dir};