Some fix in beautify pretty-printer

- In binders, {X} were printed X
- Notation toto x y := were printed Notation totox y
- Fixpoint declaration prints too much spaces
Hunt is not closed yet anyway...

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

3 files changed, 39 insertions, 47 deletions

diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 9348500721..d6c3cbb9c8 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -233,11 +233,13 @@ let surround_implicit k p =
       str"`" ++ (surround_impl b' p)
 
 let pr_binder many pr (nal,k,t) =
-  match t with
-  | CHole _ -> prlist_with_sep spc pr_lname nal
-  | _ ->
-    let s = prlist_with_sep spc pr_lname nal ++ str" : " ++ pr t in
-      hov 1 (if many then surround_binder k s else surround_implicit k s)
+      match t with
+	| CHole _ ->
+	  let s = prlist_with_sep spc pr_lname nal in
+	  hov 1 (surround_implicit k s)
+	| _ ->
+	  let s = prlist_with_sep spc pr_lname nal ++ str" : " ++ pr t in
+	  hov 1 (if many then surround_binder k s else surround_implicit k s)
 
 let pr_binder_among_many pr_c = function
   | LocalRawAssum (nal,k,t) ->
@@ -323,19 +325,27 @@ let pr_recursive_decl pr pr_dangling dangling_with_for id bl annot t c =
   pr_opt_type_spc pr t ++ str " :=" ++
   pr_sep_com (fun () -> brk(1,2)) (pr_body ltop) c
 
-let pr_fixdecl pr prd dangling_with_for ((_,id),(n,ro),bl,t,c) =
-  let annot =
-    match ro with
-	CStructRec ->
-	  if List.length bl > 1 && n <> None then
-	    spc() ++ str "{struct " ++ pr_id (snd (Option.get n)) ++ str"}"
-	  else mt()
-      | CWfRec c ->
-	  spc () ++ str "{wf " ++ pr lsimple c ++ pr_id (snd (Option.get n)) ++ str"}"
-      | CMeasureRec (m,r) ->
-	  spc () ++ str "{measure " ++ pr lsimple m ++ pr_id (snd (Option.get n)) ++
-	    (match r with None -> mt() | Some r -> str" on " ++ pr lsimple r) ++ str"}"
-  in
+let pr_guard_annot pr_aux bl (n,ro) =
+  match n with
+    | None -> mt ()
+    | Some (loc, id) ->
+      match (ro : Topconstr.recursion_order_expr) with
+	| CStructRec ->
+	  let names_of_binder = function
+	    | LocalRawAssum (nal,_,_) -> nal
+	    | LocalRawDef (_,_) -> []
+	  in let ids = List.flatten (List.map names_of_binder bl) in
+	     if List.length ids > 1 then
+	       spc() ++ str "{struct " ++ pr_id id ++ str"}"
+	     else mt()
+	| CWfRec c ->
+	  spc() ++ str "{wf " ++ pr_aux c ++ spc() ++ pr_id id ++ str"}"
+	| CMeasureRec (m,r) ->
+	  spc() ++ str "{measure " ++ pr_aux m ++ spc() ++ pr_id id++
+	    (match r with None -> mt() | Some r -> str" on " ++ pr_aux r) ++ str"}"
+
+let pr_fixdecl pr prd dangling_with_for ((_,id),ro,bl,t,c) =
+  let annot = pr_guard_annot (pr lsimple) bl ro in
     pr_recursive_decl pr prd dangling_with_for id bl annot t c
 
 let pr_cofixdecl pr prd dangling_with_for ((_,id),bl,t,c) =
diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli
index f9ed3af02f..afcdad3e49 100644
--- a/parsing/ppconstr.mli
+++ b/parsing/ppconstr.mli
@@ -51,12 +51,16 @@ val pr_with_occurrences :
   ('a -> std_ppcmds) -> 'a with_occurrences -> std_ppcmds
 val pr_red_expr :
   ('a -> std_ppcmds) * ('a -> std_ppcmds) * ('b -> std_ppcmds) * ('c -> std_ppcmds) ->
-    ('a,'b,'c) red_expr_gen -> std_ppcmds
+  ('a,'b,'c) red_expr_gen -> std_ppcmds
 val pr_may_eval :
   ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) ->
   ('c -> std_ppcmds) -> ('a,'b,'c) may_eval -> std_ppcmds
 
 val pr_glob_sort : glob_sort -> std_ppcmds
+val pr_guard_annot : (constr_expr -> std_ppcmds) ->
+  local_binder list ->
+  ('a * Names.identifier) option * recursion_order_expr ->
+  std_ppcmds
 
 val pr_binders : local_binder list -> std_ppcmds
 val pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 1fa57878d5..bf038dc3c7 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -292,28 +292,6 @@ let pr_binders_arg =
 let pr_and_type_binders_arg bl =
   pr_binders_arg bl
 
-let names_of_binder = function
-  | LocalRawAssum (nal,_,_) -> nal
-  | LocalRawDef (_,_) -> []
-
-let pr_guard_annot bl (n,ro) =
-  match n with
-  | None -> mt ()
-  | Some (loc, id) ->
-      match (ro : Topconstr.recursion_order_expr) with
-      | CStructRec ->
-          let ids = List.flatten (List.map names_of_binder bl) in
-	  if List.length ids > 1 then
-	    spc() ++ str "{struct " ++ pr_id id ++ str"}"
-	  else mt()
-      | CWfRec c ->
-	  spc() ++ str "{wf " ++ pr_lconstr_expr c ++ spc() ++
-	  pr_id id ++ str"}"
-      | CMeasureRec (m,r) ->
-	  spc() ++ str "{measure " ++ pr_lconstr_expr m ++ spc() ++
-	  pr_id id ++ (match r with None -> mt() | Some r -> str" on " ++
-	    pr_lconstr_expr r) ++ str"}"
-
 let pr_onescheme (idop,schem) =
   match schem with
   | InductionScheme (dep,ind,s) ->
@@ -419,7 +397,7 @@ let pr_statement head (id,(bl,c,guard)) =
   hov 1
     (head ++ spc() ++ pr_lident (Option.get id) ++ spc() ++
     (match bl with [] -> mt() | _ -> pr_binders bl ++ spc()) ++
-    pr_opt (pr_guard_annot bl) guard ++
+    pr_opt (pr_guard_annot pr_lconstr_expr bl) guard ++
     str":" ++ pr_spc_lconstr c)
 
 (**************************************)
@@ -635,10 +613,10 @@ let rec pr_vernac = function
   | VernacFixpoint recs ->
       let pr_onerec = function
         | ((loc,id),ro,bl,type_,def),ntn ->
-            let annot = pr_guard_annot bl ro in
-            pr_id id ++ pr_binders_arg bl ++ annot ++ spc()
+            let annot = pr_guard_annot pr_lconstr_expr bl ro in
+            pr_id id ++ pr_binders_arg bl ++ annot
             ++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_
-            ++ pr_opt (fun def -> str" :=" ++ brk(1,2) ++ pr_lconstr def) def ++
+            ++ pr_opt (fun def -> str":=" ++ brk(1,2) ++ pr_lconstr def) def ++
 	    prlist (pr_decl_notation pr_constr) ntn
       in
       hov 0 (str "Fixpoint" ++ spc() ++
@@ -806,8 +784,8 @@ let rec pr_vernac = function
       pr_hints local dbnames h pr_constr pr_constr_pattern_expr
   | VernacSyntacticDefinition (id,(ids,c),local,onlyparsing) ->
       hov 2
-        (pr_locality local ++ str"Notation " ++ pr_lident id ++
-	 prlist_with_sep spc pr_id ids ++ str" :=" ++ pr_constrarg c ++
+        (pr_locality local ++ str"Notation " ++ pr_lident id ++ spc () ++
+	 prlist (fun x -> spc() ++ pr_id x) ids ++ str":=" ++ pr_constrarg c ++
          pr_syntax_modifiers (if onlyparsing then [SetOnlyParsing] else []))
   | VernacDeclareImplicits (local,q,[]) ->
       hov 2 (pr_section_locality local ++ str"Implicit Arguments" ++ spc() ++