# HG changeset patch
# User wenzelm
# Date 1636026792 -3600
# Node ID 4a45dfee3402cd08ffbc23e7becc24c851151036
# Parent  42f358ea8deed876a85711ec1ac2df4c991182a3
prefer official Export.explode_name;
avoid string interpolation: Isabelle/Scala is closer to Isabelle/ML than Python/Perl;

diff -r 42f358ea8dee -r 4a45dfee3402 src/HOL/Tools/Mirabelle/mirabelle.scala
--- a/src/HOL/Tools/Mirabelle/mirabelle.scala	Thu Nov 04 12:43:34 2021 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle.scala	Thu Nov 04 12:53:12 2021 +0100
@@ -86,13 +86,14 @@
                   using(store.open_database_context())(db_context =>
                   {
                     for (entry <- db_context.read_export(session_hierarchy, args.theory_name, args.name)) {
-                      val prefix = args.name.split('/') match {
-                        case Array("mirabelle", action, "finalize") =>
-                          s"${action} finalize  "
-                        case Array("mirabelle", action, "goal", goal_name, line, offset) =>
-                          s"${action} goal.${goal_name} ${args.theory_name} ${line}:${offset}  "
-                        case _ => ""
-                      }
+                      val prefix =
+                        Export.explode_name(args.name) match {
+                          case List("mirabelle", action, "finalize") => action + " finalize  "
+                          case List("mirabelle", action, "goal", goal_name, line, offset) =>
+                            action + " goal." + goal_name + " " + args.theory_name + " " +
+                              line + ":" + offset + "  "
+                          case _ => ""
+                        }
                       val lines = Pretty.string_of(entry.uncompressed_yxml).trim()
                       val body = Library.prefix_lines(prefix, lines) + "\n"
                       val log_file = output_dir + Path.basic("mirabelle.log")