# HG changeset patch
# User desharna
# Date 1673534804 -3600
# Node ID fcd1df8f48fc3ffc19251e6e81b46b4aaceade2f
# Parent  7ed303c024187025d7c89dd9d27a42284c1a34b4
added session to mirabelle output directory structure

diff -r 7ed303c02418 -r fcd1df8f48fc NEWS
--- a/NEWS	Wed Jan 11 17:02:52 2023 +0000
+++ b/NEWS	Thu Jan 12 15:46:44 2023 +0100
@@ -180,6 +180,9 @@
       multp_mono_strong
       wfP_subset_mset[simp]
 
+* Mirabelle:
+  - Added session to output directory structure. Minor INCOMPATIBILITY.
+
 
 *** ML ***
 
diff -r 7ed303c02418 -r fcd1df8f48fc src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Wed Jan 11 17:02:52 2023 +0000
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Thu Jan 12 15:46:44 2023 +0100
@@ -305,12 +305,14 @@
     exhaustive_preplay proof_method_from_msg thy_index trivial pos st =
   let
     val thy = Proof.theory_of st
-    val thy_name = Context.theory_name thy
+    val thy_long_name = Context.theory_long_name thy
+    val session_name = Long_Name.qualifier thy_long_name
+    val thy_name = Long_Name.base_name thy_long_name
     val triv_str = if trivial then "[T] " else ""
     val keep =
       if keep_probs orelse keep_proofs then
         let val subdir = StringCvt.padLeft #"0" 4 (string_of_int thy_index) ^ "_" ^ thy_name in
-          Path.append output_dir (Path.basic subdir)
+          Path.append (Path.append output_dir (Path.basic session_name)) (Path.basic subdir)
           |> Isabelle_System.make_directory
           |> Path.implode
           |> (fn dir => SOME (dir, keep_probs, keep_proofs))