# HG changeset patch
# User desharna
# Date 1623494373 -7200
# Node ID bb277f37c34ae0157de523ad6a152809f82c368c
# Parent  93228ff7aa67679d72f197875bb2e29378c33a12
added warnings when defining unamed or redefining Mirabelle action

diff -r 93228ff7aa67 -r bb277f37c34a src/HOL/Tools/Mirabelle/mirabelle.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle.ML	Sat Jun 12 12:16:19 2021 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML	Sat Jun 12 12:39:33 2021 +0200
@@ -53,7 +53,10 @@
     (Symtab.empty : (action_context -> action) Symtab.table);
 in
 
-val register_action = Synchronized.change actions oo curry Symtab.update;
+fun register_action name make_action =
+  (if name = "" then error "Registering unnamed Mirabelle action" else ();
+   Synchronized.change actions (Symtab.map_default (name, make_action)
+     (fn f => (warning ("Redefining Mirabelle action: " ^ quote name); f))));
 
 fun get_action name = Symtab.lookup (Synchronized.value actions) name;