Now parsing rules of ML-declared tactics are only made available after the

corresponding Declare ML Module command. This changes essentially two
things:

1. ML plugins are forced to use the DECLARE PLUGIN statement before any
TACTIC EXTEND statement. The plugin name must be exactly the string passed to
the Declare ML Module command.

2. ML tactics are only made available after the Coq module that does the
corresponding Declare ML Module is imported. This may break a few things,
as it already broke quite some uses of omega in the stdlib.

1 files changed, 45 insertions, 0 deletions

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 3b86cf72f8..a64f32d099 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -126,6 +126,51 @@ let add_tactic_notation (local,n,prods,e) =
   Lib.add_anonymous_leaf (inTacticGrammar tacobj)
 
 (**********************************************************************)
+(* ML Tactic entries                                                  *)
+
+type atomic_entry = string * Genarg.glob_generic_argument list option
+
+type ml_tactic_grammar_obj = {
+  mltacobj_name : string;
+  (** ML-side unique name *)
+  mltacobj_prod : grammar_prod_item list list;
+  (** Grammar rules generating the ML tactic. *)
+  mltacobj_atom : atomic_entry list;
+  (** ML tactic notations whose use can be restricted to an identifier. *)
+}
+
+let extend_atomic_tactic name entries =
+  let add_atomic (id, args) = match args with
+  | None -> ()
+  | Some args ->
+    let loc = Loc.ghost in
+    let body = Tacexpr.TacAtom (loc, Tacexpr.TacExtend (loc, name, args)) in
+    Tacenv.register_atomic_ltac (Names.Id.of_string id) body
+  in
+  List.iter add_atomic entries
+
+let cache_ml_tactic_notation (_, obj) =
+  extend_ml_tactic_grammar obj.mltacobj_name obj.mltacobj_prod;
+  extend_atomic_tactic obj.mltacobj_name obj.mltacobj_atom
+
+let open_ml_tactic_notation i obj =
+  if Int.equal i 1 then cache_ml_tactic_notation obj
+
+let inMLTacticGrammar : ml_tactic_grammar_obj -> obj =
+  declare_object { (default_object "MLTacticGrammar") with
+    open_function = open_ml_tactic_notation;
+    cache_function = cache_ml_tactic_notation;
+  }
+
+let add_ml_tactic_notation name prods atomic =
+  let obj = {
+    mltacobj_name = name;
+    mltacobj_prod = prods;
+    mltacobj_atom = atomic;
+  } in
+  Lib.add_anonymous_leaf (inMLTacticGrammar obj)
+
+(**********************************************************************)
 (* Printing grammar entries                                           *)
 
 let entry_buf = Buffer.create 64