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

4 files changed, 57 insertions, 56 deletions

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
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 7409a9e80..4ea1c4e5b 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -46,6 +46,8 @@ val grammar_extend :
 
 val remove_grammars : int -> unit
 
+val camlp4_verbosity : bool -> ('a -> unit) -> 'a -> unit
+
 (* Parse a string *)
 
 val parse_string : 'a Gram.Entry.e -> string -> 'a
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index a8dd7b8aa..d38259768 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -103,7 +103,7 @@ let pr_notation pr s env =
   prlist (print_hunk pr env) unpl, level
 
 let pr_delimiters key strm =
-  let left = "`"^key^":" and right = "`" in
+  let left = "'"^key^":" and right = "'" in
   let lspace =
     if is_letter (left.[String.length left -1]) then str " " else mt () in
   let rspace =
@@ -386,6 +386,7 @@ let gentermpr gt =
   with s -> wrap_exception s
 
 (* [at_top] means ids of env must be avoided in bound variables *)
+
 let gentermpr_core at_top env t =
   gentermpr (Termast.ast_of_constr at_top env t)
 
@@ -394,4 +395,3 @@ let gentermpr_core at_top env t =
   pr_constr (Constrextern.extern_constr at_top env t)
 *)
 
-
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index e37d0d664..7313ed7bd 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -258,10 +258,9 @@ type symbol =
   | Break of int
 
 let prec_assoc = function
-  | Some(Gramext.RightA) -> (L,E)
-  | Some(Gramext.LeftA) -> (E,L)
-  | Some(Gramext.NonA) -> (L,L)
-  | None -> (L,L)   (* NONA by default *)
+  | Gramext.RightA -> (L,E)
+  | Gramext.LeftA -> (E,L)
+  | Gramext.NonA -> (L,L)
 
 let level_rule (n,p) = if p = E then n else max (n-1) 0
 
@@ -270,49 +269,50 @@ let meta_pattern m = Pmeta(m,Tany)
 
 open Symbols
 
-type white_status = NextMaybeLetter | NoSpace | AddBrk of int
+type white_status = Juxtapose | Separate of int
 
 let add_break l = function
-  | AddBrk n -> UNP_BRK (n,1) :: l
+  | Separate n -> UNP_BRK (n,1) :: l
   | _ -> l
 
 let precedence_of_entry_type = function
-  | ETConstr (n,BorderProd (left,a)) ->
+  | ETConstr (n,BorderProd (left,None)) -> (n,Prec n)
+  | ETConstr (n,BorderProd (left,Some a)) ->
       (n, let (lp,rp) = prec_assoc a in if left then lp else rp)
   | ETConstr (n,InternalProd) -> (n,E)
   | _ -> 0,E
 
+(* x = y |-> x brk = y (breaks before any symbol) *)
+(* x =S y |-> x spc =S spc y (protect from confusion; each side for symmetry)*)
+(* + { |-> + { may breaks reversibility without space but oth. not elegant *)
+(* x y |-> x spc y *)
+
 (* For old ast printer *)
 let make_hunks_ast symbols etyps from =
   let (_,l) =
   List.fold_right
     (fun it (ws,l) -> match it with
       | NonTerminal m ->
-	  let (_,lp) = precedence_of_entry_type (List.assoc m etyps) in
+	  let (n,lp) = precedence_of_entry_type (List.assoc m etyps) in
 	  let u = PH (meta_pattern (string_of_id m), None, lp) in
 	  let l' = u :: (add_break l ws) in
-(*
-	  ((if from = 10 (* lconstr *) then AddBrk 1 else NextMaybeLetter), l')
-*)
-	  (AddBrk 1, l')
+	  (Separate 1, l')
       | Terminal s ->
-(*
-	  let l' = add_break l ws in
-*)
-	  let l' = l in
-	  if from = 10 (* lconstr *) then (AddBrk 1, RO s :: l')
-	  else
-	    let n = if is_letter (s.[0]) then 1 else 0 in
-	    let s = 
-	      if (ws = NextMaybeLetter or ws = AddBrk 1)
-		& is_letter (s.[String.length s -1])
-	      then s^" "
-	      else s
-	    in
-	    (AddBrk n, RO s :: l')
+	    let n,(s,l) =
+	      if
+		is_letter (s.[0]) or 
+		is_letter (s.[String.length s -1]) or
+		is_digit (s.[String.length s -1])
+	      then
+		(* We want spaces around both sides *)
+		Separate 1,
+		if ws = Separate 0 then s^" ",l else s,add_break l ws
+	      else
+		Juxtapose, (s,l) in
+	    (n, RO s :: l)
       | Break n ->
-	    (NoSpace, UNP_BRK (n,1) :: l))
-    symbols (NoSpace,[])
+	    (Juxtapose, UNP_BRK (n,1) :: l))
+    symbols (Juxtapose,[])
   in l
 
 let make_hunks etyps symbols =
@@ -325,21 +325,21 @@ let make_hunks etyps symbols =
 	  let prec = precedence_of_entry_type (List.nth typs (i-1)) in
 	  let u = UnpMetaVar (i ,prec) in
 	  let l' = match ws with
-	    | AddBrk n -> UnpCut (PpBrk(n,1)) :: u :: l
+	    | Separate n -> UnpCut (PpBrk(n,1)) :: u :: l
 	    | _ -> u :: l in
-	  (NextMaybeLetter, l')
+	  (Separate 1, l')
       | Terminal s ->
 	  let n = if is_letter (s.[0]) then 1 else 0 in
 	  let s = 
-	    if (ws = NextMaybeLetter or ws = AddBrk 1)
+	    if (ws = Separate 1)
 	      & is_letter (s.[String.length s -1])
 	    then s^" "
 	    else s
 	  in
-	  (AddBrk n, UnpTerminal s :: l)
+	  (Separate n, UnpTerminal s :: l)
       | Break n ->
-	    (NoSpace, UnpCut (PpBrk (n,1)) :: l))
-    symbols (NextMaybeLetter,[])
+	    (Juxtapose, UnpCut (PpBrk (n,1)) :: l))
+    symbols (Juxtapose,[])
   in l
 
 let string_of_prec (n,p) =
@@ -526,9 +526,7 @@ let set_entry_type etyps (x,typ) =
   let typ = try 
     match List.assoc x etyps, typ with
       | ETConstr (n,()), (_,BorderProd (left,_)) ->
-	  (* We set an associativity telling not to change the level *)
-	  let assoc = if left then Gramext.LeftA else Gramext.RightA in
-          ETConstr (n,BorderProd (left,Some assoc))
+          ETConstr (n,BorderProd (left,None))
       | ETConstr (n,()), (_,InternalProd) -> ETConstr (n,InternalProd)
       | (ETPattern | ETIdent | ETBigint | ETOther _ | ETReference as t), _ -> t
     with Not_found -> ETConstr typ
@@ -576,7 +574,7 @@ let open_notation i (_,(oldse,prec,ntn,scope,pat,onlyparse,df)) =
     if not b then
       Symbols.declare_notation_interpretation ntn scope pat prec df;
     if not b & not onlyparse then
-      Symbols.declare_uninterpretation (NotationRule (ntn,scope)) pat
+      Symbols.declare_uninterpretation (NotationRule (scope,ntn)) pat
   end
 
 let cache_notation o =