From 870075f34dd9fa5792bfbf413afd3b96f17e76a0 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Fri, 8 Aug 2008 13:18:42 +0200
Subject: Imported Upstream version 8.2~beta4+dfsg

---
 parsing/egrammar.ml | 34 ++++++++++++++++++++--------------
 1 file changed, 20 insertions(+), 14 deletions(-)

(limited to 'parsing/egrammar.ml')

diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 9416bff2..825d1af0 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: egrammar.ml 10987 2008-05-26 12:28:36Z herbelin $ *)
+(* $Id: egrammar.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
 
 open Pp
 open Util
@@ -114,27 +114,33 @@ let make_constr_prod_item univ assoc from forpat = function
 let prepare_empty_levels entry (pos,p4assoc,name,reinit) =
   grammar_extend entry pos reinit [(name, p4assoc, [])]
 
-let extend_constr entry (n,assoc,pos,p4assoc,name,reinit) mkact (forpat,pt) =
+let pure_sublevels level symbs =
+  map_succeed (function
+  | Gramext.Snterml (_,n) when Some (int_of_string n) <> level ->
+      int_of_string n
+  | _ ->
+      failwith "") symbs
+
+let extend_constr (entry,level) (n,assoc) mkact forpat pt =
   let univ = get_univ "constr" in
   let pil = List.map (make_constr_prod_item univ assoc n forpat) pt in
   let (symbs,ntl) = List.split pil in
-  let needed_levels = register_empty_levels forpat symbs in
+  let pure_sublevels = pure_sublevels level symbs in
+  let needed_levels = register_empty_levels forpat pure_sublevels in
+  let pos,p4assoc,name,reinit = find_position forpat assoc level in
   List.iter (prepare_empty_levels entry) needed_levels;
   grammar_extend entry pos reinit [(name, p4assoc, [symbs, mkact ntl])]
 
 let extend_constr_notation (n,assoc,ntn,rule) =
   (* Add the notation in constr *)
   let mkact loc env = CNotation (loc,ntn,List.map snd env) in
-  let (e,level) = get_constr_entry false (ETConstr (n,())) in
-  let pos,p4assoc,name,reinit = find_position false assoc level in
-  extend_constr e (ETConstr(n,()),assoc,pos,p4assoc,name,reinit)
-    (make_constr_action mkact) (false,rule);
+  let e = get_constr_entry false (ETConstr (n,())) in
+  extend_constr e (ETConstr(n,()),assoc) (make_constr_action mkact) false rule;
   (* Add the notation in cases_pattern *)
   let mkact loc env = CPatNotation (loc,ntn,List.map snd env) in
-  let (e,level) = get_constr_entry true (ETConstr (n,())) in
-  let pos,p4assoc,name,reinit = find_position true assoc level in
-  extend_constr e (ETConstr (n,()),assoc,pos,p4assoc,name,reinit)
-    (make_cases_pattern_action mkact) (true,rule)
+  let e = get_constr_entry true (ETConstr (n,())) in
+  extend_constr e (ETConstr (n,()),assoc) (make_cases_pattern_action mkact)
+    true rule
 
 (**********************************************************************)
 (** Making generic actions in type generic_argument                   *)
@@ -228,7 +234,7 @@ let rec interp_entry_name up_level s =
       try get_entry (get_univ "prim") s
       with _ ->
       try get_entry (get_univ "constr") s
-      with _ -> error ("Unknown entry "^s)
+      with _ -> error ("Unknown entry "^s^".")
     in
     let o = object_of_typed_entry e in
     let t = type_of_typed_entry e in
@@ -248,7 +254,7 @@ let get_tactic_entry n =
   else if 1<=n && n<5 then
     weaken_entry Tactic.tactic_expr, Some (Gramext.Level (string_of_int n))
   else 
-    error ("Invalid Tactic Notation level: "^(string_of_int n))
+    error ("Invalid Tactic Notation level: "^(string_of_int n)^".")
 
 (* Declaration of the tactic grammar rule *)
 
@@ -261,7 +267,7 @@ let add_tactic_entry (key,lev,prods,tac) =
   let rules = 
     if lev = 0 then begin
       if not (head_is_ident prods) then
-	error "Notation for simple tactic must start with an identifier";
+	error "Notation for simple tactic must start with an identifier.";
       let mkact s tac loc l =
 	(TacAlias(loc,s,l,tac):raw_atomic_tactic_expr) in
       make_rule univ (mkact key tac) mkprod prods
-- 
cgit v1.2.3