From f6c7ba13084782457d1a41c1e8d573479b105fa0 Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 4 Dec 2002 22:45:00 +0000 Subject: Correction divers bugs d'affichage; explicitation du niveau de grammaire quand mentionn explicitement par l'utilisateur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3377 85f007b7-540e-0410-9357-904b9bb8a0f7 --- parsing/pcoq.ml4 | 33 +++++++++++++++++---------------- 1 file changed, 17 insertions(+), 16 deletions(-) (limited to 'parsing/pcoq.ml4') diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 72eb7dca1..96b358402 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -122,14 +122,17 @@ module Gram = end +let camlp4_verbosity silent f x = + let a = !Gramext.warning_verbose in + Gramext.warning_verbose := silent; + f x; + Gramext.warning_verbose := a + (* This extension command is used by the Grammar constr *) let grammar_extend te pos rls = camlp4_state := ByGrammar (Gramobj.weaken_entry te,pos,rls) :: !camlp4_state; - let a = !Gramext.warning_verbose in - Gramext.warning_verbose := Options.is_verbose (); - G.extend te pos rls; - Gramext.warning_verbose := a + camlp4_verbosity (Options.is_verbose ()) (G.extend te pos) rls (* n is the number of extended entries (not the number of Grammar commands!) to remove. *) @@ -503,22 +506,20 @@ let camlp4_assoc = function | Some Gramext.NonA | Some Gramext.RightA -> Gramext.RightA | None | Some Gramext.LeftA -> Gramext.LeftA -(* Official Coq convention *) -let coq_assoc = function - | None -> Gramext.LeftA - | Some a -> a - let adjust_level assoc = function - (* If no associativity constraints, adopt the current one *) + (* If NonA on the right-hand side, set to NEXT *) | (n,BorderProd (false,Some Gramext.NonA)) -> Some None - | (n,BorderProd (_,Some Gramext.NonA)) -> None - (* Otherwise, deal with the current one *) - | (n,BorderProd (_,a)) when coq_assoc a = camlp4_assoc assoc -> None - | (n,BorderProd (left,a)) -> - let a = coq_assoc a in + (* If NonA on the left-hand side, adopt the current assoc ?? *) + | (n,BorderProd (true,Some Gramext.NonA)) -> None + (* Associativity is None means force the level *) + | (n,BorderProd (_,None)) -> Some (Some n) + (* If the expected assoc is the current one, SELF on both sides *) + | (n,BorderProd (_,Some a)) when a = camlp4_assoc assoc -> None + (* Otherwise, force the level, n or n-1, according to expected assoc *) + | (n,BorderProd (left,Some a)) -> if (left & a = Gramext.LeftA) or ((not left) & a = Gramext.RightA) then Some (Some n) else Some (Some (n-1)) - | (8,InternalProd) -> None +(* | (8,InternalProd) -> None (* Or (Some 8) for factorization ? *)*) | (n,InternalProd) -> Some (Some n) let compute_entry allow_create adjust = function -- cgit v1.2.3