Nouvelle solution pour le probleme d'effacement des niveaux vides de operconstr et pattern: plus de niveaux vides

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

3 files changed, 28 insertions, 29 deletions

diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index eb61a70bd..e97b3d5e4 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -268,7 +268,7 @@ let extend_entry univ (te, etyp, pos, name, ass, p4ass, rls) =
 (* Defines new entries. If the entry already exists, check its type *)
 let define_entry univ {ge_name=typ; gl_assoc=ass; gl_rules=rls} =
   let e,lev,keepassoc = get_constr_entry false typ in
-  let pos,p4ass,name = find_position keepassoc ass lev in
+  let pos,p4ass,name = find_position false keepassoc ass lev in
   (e,typ,pos,name,ass,p4ass,rls)
 
 (* Add a bunch of grammar rules. Does not check if it is well formed *)
@@ -307,12 +307,13 @@ let extend_constr entry (n,assoc,pos,p4assoc,name) make_act (forpat,pt) =
 let extend_constr_notation (n,assoc,ntn,rule) =
   let mkact loc env = CNotation (loc,ntn,List.map snd env) in
   let (e,level,keepassoc) = get_constr_entry false (ETConstr (n,())) in
-  let pos,p4assoc,name = find_position keepassoc assoc level in
+  let pos,p4assoc,name = find_position false keepassoc assoc level in
   extend_constr e (ETConstr(n,()),assoc,pos,p4assoc,name)
     (make_act mkact) (false,rule);
   if not !Options.v7 then
   let mkact loc env = CPatNotation (loc,ntn,List.map snd env) in
   let (e,level,keepassoc) = get_constr_entry true (ETConstr (n,())) in
+  let pos,p4assoc,name = find_position true keepassoc assoc level in
   extend_constr e (ETConstr (n,()),assoc,pos,p4assoc,name)
     (make_act_in_cases_pattern mkact) (true,rule)
     
@@ -378,7 +379,7 @@ let add_tactic_entries gl =
   let f (s,l,tac) =
     make_rule univ (make_act s tac) (make_vprod_item "tactic") l in
   let rules = List.map f gl in
-  let _ = find_position true None None (* for synchronisation with remove *) in
+  let _ = find_position true true None None (* to synchronise with remove *) in
   grammar_extend Tactic.simple_tactic None [(None, None, List.rev rules)]
 
 let extend_grammar gram =
@@ -411,27 +412,26 @@ let factorize_grams l1 l2 =
 
 let number_of_entries gcl =
   List.fold_left
-    (fun (n,l) -> function
+    (fun n -> function
       | Notation _ -> 
-          (if !Options.v7 then n + 1
-          else n + 2 (* 1 for operconstr, 1 for pattern *)), l + 1
+          if !Options.v7 then n + 1
+	  else n + 2 (* 1 for operconstr, 1 for pattern *)
       | Grammar gc ->
-          n + (List.length gc.gc_entries), l + (List.length gc.gc_entries)
-      | TacticGrammar _ -> n + 1, l + 1)
-    (0,0) gcl
+          n + (List.length gc.gc_entries)
+      | TacticGrammar _ -> n + 1)
+    0 gcl
 
 let unfreeze (grams, lex) =
   let (undo, redo, common) = factorize_grams !grammar_state grams in
-  let n,l = number_of_entries undo in
+  let n = number_of_entries undo in
   remove_grammars n;
-  remove_levels l;
-  reinit_levels ();
+  remove_levels n;
   grammar_state := common;
   Lexer.unfreeze lex;
   List.iter extend_grammar (List.rev redo)
  
 let init_grammar () =
-  remove_grammars (fst (number_of_entries !grammar_state));
+  remove_grammars (number_of_entries !grammar_state);
   grammar_state := []
 
 let init () =
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 3930c270a..280c501a9 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -426,14 +426,6 @@ let reset_all_grammars () =
   f Vernac_.vernac;
   Lexer.init()
 
-let reinit_levels () =
-  if not !Options.v7 then begin
-  (* Ensure that primitive levels exist even if emptied by rule deletion *)
-    G.extend Constr.pattern (Some(Gramext.Before "0")) [(Some "1",None,[])];
-    G.extend Constr.operconstr (Some(Gramext.After "10")) [(Some "9",None,[])];
-    G.extend Constr.pattern (Some(Gramext.After "10")) [(Some "9",None,[])]
-  end
-
 let main_entry = Gram.Entry.create "vernac"
 
 GEXTEND Gram
@@ -561,8 +553,15 @@ let default_levels_v8 =
    1,Gramext.LeftA;
    0,Gramext.RightA]
 
+let default_pattern_levels_v8 =
+  [250,Gramext.LeftA;
+   10,Gramext.LeftA;
+   0,Gramext.RightA]
+
 let level_stack = 
-  ref [if !Options.v7 then default_levels_v7 else default_levels_v8]
+  ref 
+    [if !Options.v7 then (default_levels_v7, default_levels_v7)
+     else (default_levels_v8, default_pattern_levels_v8)]
 
 (* At a same level, LeftA takes precedence over RightA and NoneA *)
 (* In case, several associativity exists for a level, we make two levels, *)
@@ -590,10 +589,10 @@ let error_level_assoc p current expected =
      pr_assoc current ++ str " associative while it is now expected to be " ++
      pr_assoc expected ++ str " associative")
 
-let find_position other assoc lev =
+let find_position forpat other assoc lev =
   let default =
     if !Options.v7 then (10,Gramext.RightA) else (200,Gramext.RightA) in
-  let current = List.hd !level_stack in 
+  let ccurrent,pcurrent as current = List.hd !level_stack in 
   match lev with
   | None ->
       level_stack := current :: !level_stack;
@@ -621,8 +620,10 @@ let find_position other assoc lev =
       in
       try
 	(* Create the entry *)
-        let current = List.hd !level_stack in
-        level_stack := add_level default current :: !level_stack;
+	let updated =
+	  if forpat then (ccurrent, add_level default pcurrent)
+	  else (add_level default ccurrent, pcurrent) in
+        level_stack := updated:: !level_stack;
 	let assoc = create_assoc assoc in
         Some (Gramext.After (constr_level2 !after)),
 	Some assoc, Some (constr_level2 (n,assoc))
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 71657fafa..1bd6d4e7c 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -46,8 +46,6 @@ val grammar_extend :
 
 val remove_grammars : int -> unit
 
-val reinit_levels : unit -> unit
-
 val camlp4_verbosity : bool -> ('a -> unit) -> 'a -> unit
 
 (* Parse a string *)
@@ -183,7 +181,7 @@ val reset_all_grammars : unit -> unit
 (* Registering/resetting the level of an entry *)
 
 val find_position : 
-  bool -> Gramext.g_assoc option -> int option ->
+  bool -> bool -> Gramext.g_assoc option -> int option ->
     Gramext.position option * Gramext.g_assoc option * string option
 
 val remove_levels : int -> unit