MAJ delimiters et niveaux d'associativite

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

3 files changed, 24 insertions, 23 deletions

diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 5b57774920..17d9736211 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -47,22 +47,25 @@ let symbolic_level = function
   | 11 -> "pattern", None
   | n -> "constr", Some n
 
-let numeric_levels = ref [8;1;0]
-
-exception Found
-
-let find_position n =
-  let after = ref 8 in
-  let rec add_level q = function
-    | p::l when p > n -> p :: add_level p l
-    | p::l when p = n -> raise Found
-    | l -> after := q; n::l
-  in
-  try
-    numeric_levels := add_level 8 !numeric_levels;
-    Gramext.After (constr_level !after)
-  with
-      Found -> Gramext.Level (constr_level n)
+let numeric_levels =
+  ref [8,Some Gramext.RightA; 1,None; 0,None ]
+
+exception Found of Gramext.g_assoc option
+
+let find_position assoc = function
+  | None -> None, assoc
+  | Some n ->
+      let after = ref 8 in
+      let rec add_level q = function
+        | (p,_ as pa)::l when p > n -> pa :: add_level p l
+        | (p,a)::l when p = n -> raise (Found a)
+        | l -> after := q; (n,assoc)::l
+      in
+      try
+        numeric_levels := add_level 8 !numeric_levels;
+        Some (Gramext.After (constr_level !after)), assoc
+      with
+          Found a -> Some (Gramext.Level (constr_level n)), a
 
 (* Interpretation of the right hand side of grammar rules *)
 
@@ -179,7 +182,7 @@ let extend_entry univ (te, etyp, pos, name, ass, rls) =
 let define_entry univ {ge_name=n; gl_assoc=ass; gl_rules=rls} =
   let typ = explicitize_entry (fst univ) n in
   let e,lev = entry_of_type true typ in
-  let pos = option_app find_position lev in
+  let pos,ass = find_position ass lev in
   let name = option_app constr_level lev in
   (e,typ,pos,name,ass,rls)
 
@@ -216,19 +219,16 @@ let extend_constr entry pos (level,assoc) make_act pt =
   let act = make_act ntl in
   grammar_extend entry pos [(level, assoc, [symbs, act])]
 
-let constr_entry name =
-  object_of_typed_entry (get_entry (get_univ "constr") name)
-
 let extend_constr_notation (n,assoc,ntn,rule) =
   let mkact loc env = CNotation (loc,ntn,env) in
   let (e,level) = entry_of_type false (ETConstr ((n,Ppextend.E),Some n)) in
-  let pos = option_app find_position level in
+  let pos,assoc = find_position assoc level in
   extend_constr e pos (option_app constr_level level,assoc) 
     (make_act mkact) rule
 
 let extend_constr_delimiters (sc,rule,pat_rule) =
   let mkact loc env = CDelimiters (loc,sc,snd (List.hd env)) in
-  extend_constr (constr_entry "constr") (Some (Gramext.Level "top"))
+  extend_constr Constr.constr (Some (Gramext.Level "0"))
     (None,None)
     (make_act mkact) rule;
   let mkact loc env = CPatDelimiters (loc,sc,snd (List.hd env)) in
diff --git a/parsing/extend.ml b/parsing/extend.ml
index 2e4eea4b0f..70704f0195 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -162,6 +162,7 @@ let explicitize_entry univ nt =
   | "constr8" | "constr" -> ETConstr ((8,E),Some 8)
   | "constr9" -> ETConstr ((9,E),Some 9)
   | "constr10" | "lconstr" -> ETConstr ((10,E),Some 10)
+  | "pattern" -> ETPattern
   | "ident" -> ETIdent
   | "global" -> ETReference
   | _ -> ETOther (univ,nt)
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index d042f8c915..4d675a0828 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -226,7 +226,7 @@ GEXTEND Gram
      | IDENT "Open"; IDENT "Scope"; sc = IDENT -> VernacOpenScope sc
 
      | IDENT "Delimits"; IDENT "Scope"; sc = IDENT; "with"; key = IDENT ->
-	 VernacDelimiters (sc,("'"^key^":","'"))
+	 VernacDelimiters (sc,key)
 
      | IDENT "Arguments"; IDENT "Scope"; qid = global;
          "["; scl = LIST0 opt_scope; "]" -> VernacArgumentsScope (qid,scl)