# HG changeset patch
# User wenzelm
# Date 1621074788 -7200
# Node ID 3ab18af9b2b5bec8df65e098c4da5905f81f235c
# Parent  8444d4ff56463cb312269015663051cc44d3d02f
clarified signature;

diff -r 8444d4ff5646 -r 3ab18af9b2b5 src/HOL/Tools/Mirabelle/mirabelle.scala
--- a/src/HOL/Tools/Mirabelle/mirabelle.scala	Sat May 15 12:25:24 2021 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.scala	Sat May 15 12:33:08 2021 +0200
@@ -35,10 +35,11 @@
 
   /* exported log content */
 
-  def mirabelle_export(index: Int): String = "mirabelle/" + index
-
   object Log
   {
+    def export_name(index: Int, theory: String = ""): String =
+      Export.compound_name(theory, "mirabelle/" + index)
+
     val separator = "\n------------------\n"
 
     sealed abstract class Entry { def print: String }
@@ -114,12 +115,12 @@
           theory <- theories
           if !seen_theories(theory)
           index <- 1 to actions.length
-          export <- db_context.read_export(session_hierarchy, theory, mirabelle_export(index))
+          export <- db_context.read_export(session_hierarchy, theory, Log.export_name(index))
           body = export.uncompressed_yxml
           if body.nonEmpty
         } {
           seen_theories += theory
-          val export_name = Export.compound_name(theory, mirabelle_export(index))
+          val export_name = Log.export_name(index, theory = theory)
           val log = body.map(Log.entry(export_name, _))
           val log_dir = Isabelle_System.make_directory(output_dir + Path.basic(theory))
           val log_file = log_dir + Path.basic("mirabelle" + index).log
diff -r 8444d4ff5646 -r 3ab18af9b2b5 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Sat May 15 12:25:24 2021 +0200
+++ b/src/Pure/Thy/export.scala	Sat May 15 12:33:08 2021 +0200
@@ -82,7 +82,8 @@
   def message(msg: String, theory_name: String, name: String): String =
     msg + " " + quote(name) + " for theory " + quote(theory_name)
 
-  def compound_name(a: String, b: String): String = a + ":" + b
+  def compound_name(a: String, b: String): String =
+    if (a.isEmpty) b else a + ":" + b
 
   def empty_entry(theory_name: String, name: String): Entry =
     Entry("", theory_name, name, false, Future.value(false, Bytes.empty), XML.Cache.none)