From f0d9c9cb04c15147f28fbd47a3a2c84f5c2f50d2 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 29 Nov 2002 21:14:21 +0000
Subject: Synchro de la table des niveaux avec les sections

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3341 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/egrammar.ml | 21 ++++++++++++++++-----
 1 file changed, 16 insertions(+), 5 deletions(-)

diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index f294f70799..42a23b4c85 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -47,10 +47,11 @@ let constr_level = function
 
 let constr_prod_level = function
   | 8 -> "top"
+  | 4 -> "4L"
   | n -> string_of_int n
 
-let numeric_levels =
-  ref [8,Gramext.RightA; 1,Gramext.RightA; 0,Gramext.RightA]
+let default_levels = [8,Gramext.RightA; 1,Gramext.RightA; 0,Gramext.RightA]
+let level_stack = ref [default_levels]
 
 (* At a same level, LeftA takes precedence over RightA and NoneA *)
 (* In case, several associativity exists for a level, we make two levels, *)
@@ -64,8 +65,12 @@ let admissible_assoc = function
   | Gramext.RightA, Gramext.LeftA -> false
   | _ -> true
 
-let find_position other assoc = function
-  | None -> None, (if other then assoc else None), None
+let find_position other assoc lev =
+  let current = List.hd !level_stack in 
+  match lev with
+  | None ->
+      level_stack := current :: !level_stack;
+      None, (if other then assoc else None), None
   | Some n ->
       let assoc = out_some assoc in
       if n = 8 & assoc = Gramext.LeftA then 
@@ -88,14 +93,19 @@ let find_position other assoc = function
       in
       try
 	(* Create the entry *)
-        numeric_levels := add_level (8,Gramext.RightA) !numeric_levels;
+        let current = List.hd !level_stack in
+        level_stack := add_level (8,Gramext.RightA) current :: !level_stack;
         Some (Gramext.After (constr_level !after)),
 	Some assoc, Some (constr_level (n,assoc))
       with
           Found a ->
+            level_stack := current :: !level_stack;
 	    (* Just inherit the existing associativity and name (None) *)
 	    Some (Gramext.Level (constr_level (n,a))), None, None
 
+let remove_levels n =
+  level_stack := snd (list_chop n !level_stack)
+
 (* Interpretation of the right hand side of grammar rules *)
 
 (* When reporting errors, we add the name of the grammar rule that failed *)
@@ -327,6 +337,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
   grammar_extend Tactic.simple_tactic None [(None, None, List.rev rules)]
 
 let extend_grammar gram =
-- 
cgit v1.2.3