- Cleaning (unification of ML names, removal of obsolete code,

  reorganization of code) and documentation (in pcoq.mli) of the code
  for parsing extensions (TACTIC/VERNAC/ARGUMENT EXTEND, Tactic
  Notation, Notation); merged the two copies of interp_entry_name to
  avoid they diverge.  
- Added support in Tactic Notation for ne_..._list_sep in general and
  for (ne_)ident_list(_sep) in particular.



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

4 files changed, 40 insertions, 26 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index ed21213ef..4fb56dfd6 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -939,7 +939,7 @@ in
                        | InSet  -> "_rec_nodep"
                        | InType -> "_rect_nodep")
                 ) in
-            let newid = (string_of_id (Pcoq.coerce_global_to_id y))^suffix in
+            let newid = (string_of_id (coerce_reference_to_id y))^suffix in
             let newref = (dummy_loc,id_of_string newid) in
           ((newref,x,y,z)::l1),l2
       | EqualityScheme  x -> l1,(x::l2)
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index c0105c8b3..09b76d3f3 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -28,7 +28,7 @@ open Notation
 (**********************************************************************)
 (* Tokens                                                             *)
 
-let cache_token (_,s) = Compat.using Pcoq.lexer ("", s)
+let cache_token (_,s) = add_token ("", s)
 
 let (inToken, outToken) =
   declare_object {(default_object "TOKEN") with
@@ -43,15 +43,20 @@ let add_token_obj s = Lib.add_anonymous_leaf (inToken s)
 (**********************************************************************)
 (* Tactic Notation                                                    *)
 
+let interp_prod_item lev = function
+  | TacTerm s -> GramTerminal s
+  | TacNonTerm (loc, nt, po) ->
+      let sep = match po with Some (_,sep) -> sep | _ -> "" in
+      let (etyp, e) = interp_entry_name (Some lev) nt sep in
+      GramNonTerminal (loc, etyp, e, Option.map fst po)
+
 let make_terminal_status = function
-  | VTerm s -> Some s
-  | VNonTerm _ -> None
-
-let rec make_tags lev = function
-  | VTerm s :: l -> make_tags lev l
-  | VNonTerm (loc, nt, po) :: l ->
-      let (etyp, _) = Egrammar.interp_entry_name lev nt in
-      etyp :: make_tags lev l
+  | GramTerminal s -> Some s
+  | GramNonTerminal _ -> None
+
+let rec make_tags = function
+  | GramTerminal s :: l -> make_tags l
+  | GramNonTerminal (loc, etyp, _, po) :: l -> etyp :: make_tags l
   | [] -> []
 
 let cache_tactic_notation (_,(pa,pp)) =
@@ -73,11 +78,11 @@ let (inTacticGrammar, outTacticGrammar) =
        export_function = (fun x -> Some x)}
 
 let cons_production_parameter l = function
-  | VTerm _ -> l
-  | VNonTerm (_,_,ido) -> Option.List.cons ido l
+  | GramTerminal _ -> l
+  | GramNonTerminal (_,_,_,ido) -> Option.List.cons ido l
 
 let rec tactic_notation_key = function
-  | VTerm id :: _ -> id
+  | GramTerminal id :: _ -> id
   | _ :: l -> tactic_notation_key l
   | [] -> "terminal_free_notation"
 
@@ -86,7 +91,8 @@ let rec next_key_away key t =
   else key
 
 let add_tactic_notation (n,prods,e) =
-  let tags = make_tags n prods in
+  let prods = List.map (interp_prod_item n) prods in
+  let tags = make_tags prods in
   let key = next_key_away (tactic_notation_key prods) tags in
   let pprule = (key,tags,(n,List.map make_terminal_status prods)) in
   let ids = List.fold_left cons_production_parameter [] prods in
@@ -570,19 +576,19 @@ let is_not_small_constr = function
   | _ -> false
 
 let rec define_keywords_aux = function
-    NonTerm(_,Some(_,e)) as n1 :: Term("IDENT",k) :: l
+    GramConstrNonTerminal(e,Some _) as n1 :: GramConstrTerminal("IDENT",k) :: l
       when is_not_small_constr e ->
       message ("Defining '"^k^"' as keyword");
       Lexer.add_token("",k);
-      n1 :: Term("",k) :: define_keywords_aux l
+      n1 :: GramConstrTerminal("",k) :: define_keywords_aux l
   | n :: l -> n :: define_keywords_aux l
   | [] -> []
 
 let define_keywords = function
-    Term("IDENT",k)::l ->
+    GramConstrTerminal("IDENT",k)::l ->
       message ("Defining '"^k^"' as keyword");
       Lexer.add_token("",k);
-      Term("",k) :: define_keywords_aux l
+      GramConstrTerminal("",k) :: define_keywords_aux l
   | l -> define_keywords_aux l
 
 let make_production etyps symbols =
@@ -591,9 +597,9 @@ let make_production etyps symbols =
       (fun t l -> match t with
         | NonTerminal m ->
 	    let typ = List.assoc m etyps in
-	    NonTerm (typ, Some (m,typ)) :: l
+	    GramConstrNonTerminal (typ, Some m) :: l
         | Terminal s ->
-	    Term (terminal s) :: l
+	    GramConstrTerminal (terminal s) :: l
         | Break _ ->
             l
         | SProdList (x,sl) ->
@@ -606,7 +612,7 @@ let make_production etyps symbols =
               | _ ->
                   error "Component of recursive patterns in notation must be constr." in
             let typ = ETConstrList (y,sl) in
-            NonTerm (typ, Some (x,typ)) :: l)
+            GramConstrNonTerminal (typ, Some x) :: l)
       symbols [] in
   define_keywords prod
 
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index d4b61eb00..4973cdfe6 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -24,7 +24,7 @@ val add_token_obj : string -> unit
 (* Adding a tactic notation in the environment *)
 
 val add_tactic_notation : 
-  int * grammar_production list * raw_tactic_expr -> unit
+  int * grammar_tactic_prod_item_expr list * raw_tactic_expr -> unit
 
 (* Adding a (constr) notation in the environment*)
 
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 94ebce9ea..47b36ede0 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -171,9 +171,17 @@ type inductive_expr =
 
 type module_binder = bool option * lident list * module_type_ast
 
-type grammar_production =
-  | VTerm of string
-  | VNonTerm of loc * string * Names.identifier option
+type grammar_tactic_prod_item_expr =
+  | TacTerm of string
+  | TacNonTerm of loc * string * (Names.identifier * string) option
+
+type syntax_modifier =
+  | SetItemLevel of string list * production_level
+  | SetLevel of int
+  | SetAssoc of Gramext.g_assoc
+  | SetEntryType of string * simple_constr_prod_entry_key
+  | SetOnlyParsing
+  | SetFormat of string located
 
 type proof_end =
   | Admitted
@@ -191,7 +199,7 @@ type vernac_expr =
   | VernacTimeout of int * vernac_expr
 
   (* Syntax *) 
-  | VernacTacticNotation of int * grammar_production list * raw_tactic_expr
+  | VernacTacticNotation of int * grammar_tactic_prod_item_expr list * raw_tactic_expr
   | VernacSyntaxExtension of locality_flag * (lstring * syntax_modifier list)
   | VernacOpenCloseScope of (locality_flag * bool * scope_name)
   | VernacDelimiters of scope_name * lstring