# HG changeset patch
# User wenzelm
# Date 1628189874 -7200
# Node ID e4575152b525c7c6e1368702be8f6ec2dbcd1573
# Parent  5fc39193887352f4b955bc78f42f5f022053735e# Parent  54a108beed3edbfb7f838f926d8328357edb3a2b
merged

diff -r 54a108beed3e -r e4575152b525 src/HOL/Tools/Mirabelle/mirabelle.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle.ML	Thu Aug 05 20:57:19 2021 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML	Thu Aug 05 20:57:54 2021 +0200
@@ -9,7 +9,8 @@
 sig
   (*core*)
   type action_context =
-    {index: int, name: string, arguments: Properties.T, timeout: Time.time, output_dir: Path.T}
+    {index: int, label: string, name: string, arguments: Properties.T, timeout: Time.time,
+     output_dir: Path.T}
   type command =
     {theory_index: int, name: string, pos: Position.T, pre: Proof.state, post: Toplevel.state}
   type action = {run_action: command -> string, finalize: unit -> string}
@@ -37,9 +38,23 @@
 val keywords = Keyword.no_command_keywords (Thy_Header.get_keywords \<^theory>);
 
 fun read_actions str =
-  Token.read_body keywords
-    (Parse.enum ";" (Parse.name -- Sledgehammer_Commands.parse_params))
-    (Symbol_Pos.explode0 str);
+  let
+    val actions = Token.read_body keywords
+      (Parse.enum ";" (Parse.name -- Sledgehammer_Commands.parse_params))
+      (Symbol_Pos.explode0 str)
+    fun split_name_label (name, args) labels =
+        (case String.tokens (fn c => c = #".") name of
+          [name] => (("", name, args), labels)
+        | [label, name] =>
+          (if Symtab.defined labels label then
+             error ("Action label '" ^ label ^ "' already defined.")
+           else
+             ();
+           ((label, name, args), Symtab.insert_set label labels))
+        | _ => error "Cannot parse action")
+  in
+    Option.map (fn xs => fst (fold_map split_name_label xs Symtab.empty)) actions
+  end
 
 
 (* actions *)
@@ -47,7 +62,8 @@
 type command =
   {theory_index: int, name: string, pos: Position.T, pre: Proof.state, post: Toplevel.state};
 type action_context =
-  {index: int, name: string, arguments: Properties.T, timeout: Time.time, output_dir: Path.T};
+  {index: int, label: string, name: string, arguments: Properties.T, timeout: Time.time,
+   output_dir: Path.T};
 type action = {run_action: command -> string, finalize: unit -> string};
 
 local
@@ -78,8 +94,8 @@
     if Exn.is_interrupt exn then Exn.reraise exn
     else print_exn exn;
 
-fun make_action_path (context as {index, name, ...} : action_context) =
-  Path.basic (string_of_int index ^ "." ^ name);
+fun make_action_path ({index, label, name, ...} : action_context) =
+  Path.basic (if label = "" then string_of_int index ^ "." ^ name else label);
 
 fun finalize_action ({finalize, ...} : action) context =
   let
@@ -200,15 +216,15 @@
             end;
 
           (* initialize actions *)
-          val contexts = actions |> map_index (fn (n, (name, args)) =>
+          val contexts = actions |> map_index (fn (n, (label, name, args)) =>
             let
               val make_action = the (get_action name);
-              val action_subdir = string_of_int n ^ "." ^ 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 context =
-                {index = n, name = name, arguments = args, timeout = mirabelle_timeout,
-                 output_dir = output_dir};
+                {index = n, label = label, name = name, arguments = args,
+                 timeout = mirabelle_timeout, output_dir = output_dir};
             in
               (make_action context, context)
             end);