Added a generic handler of Ltac quotations, based on the existing

syntax constr:foo and ipattern:bar (which is not very nice for
parsing, b.t.w.).

Now one is able to dynamically add quotations of the form name:...
that will use the provided function to create a dynamically typed
argument.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16611 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 35 insertions, 0 deletions

diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml
index 9905a5ad4..2e83c2b6b 100644
--- a/parsing/egramcoq.ml
+++ b/parsing/egramcoq.ml
@@ -343,3 +343,30 @@ let with_grammar_rule_protection f x =
     let reraise = Errors.push reraise in
     let () = unfreeze fs in
     raise reraise
+
+(**********************************************************************)
+(** Ltac quotations                                                   *)
+
+let ltac_quotations = ref String.Set.empty
+
+let create_ltac_quotation name cast wit e =
+  let () =
+    if String.Set.mem name !ltac_quotations then
+      failwith ("Ltac quotation " ^ name ^ " already registered")
+  in
+  let () = ltac_quotations := String.Set.add name !ltac_quotations in
+(*   let level = Some "1" in *)
+  let level = None in
+  let assoc = Some (of_coq_assoc Extend.RightA) in
+  let rule = [
+    gram_token_of_string name;
+    gram_token_of_string ":";
+    symbol_of_prod_entry_key (Agram (Gram.Entry.obj e));
+  ] in
+  let action v _ _ loc =
+    let loc = !@loc in
+    let arg = TacGeneric (Genarg.in_gen (Genarg.rawwit wit) (cast (loc, v))) in
+    TacArg (loc, arg)
+  in
+  let gram = (level, assoc, [rule, Gram.action action]) in
+  maybe_uncurry (Gram.extend Tactic.tactic_expr) (None, [gram])
diff --git a/parsing/egramcoq.mli b/parsing/egramcoq.mli
index 91a636306..7cf3bab69 100644
--- a/parsing/egramcoq.mli
+++ b/parsing/egramcoq.mli
@@ -66,3 +66,11 @@ val recover_notation_grammar :
   notation_var_internalization_type list * notation_grammar
 
 val with_grammar_rule_protection : ('a -> 'b) -> 'a -> 'b
+
+(** Adding tactic quotations *)
+
+val create_ltac_quotation : string -> ('grm Loc.located -> 'raw) ->
+  ('raw, 'glb, 'top) genarg_type -> 'grm Gram.entry -> unit
+(** [create_ltac_quotation name f wit e] adds a quotation rule to Ltac, that is,
+    Ltac grammar now accepts arguments of the form ["name" ":" <e>], and
+    generates a generic argument using [f] on the entry parsed by [e]. *)