New spacing/formatting in Locate Notation, Print Scopes, Print Visibility.

4 files changed, 16 insertions, 21 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index 04856a30f2..d57c4f3abf 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1986,7 +1986,7 @@ let pr_scope_classes sc =
       spc() ++ prlist_with_sep spc pr_scope_class l)
 
 let pr_notation_info prglob ntn c =
-  str "\"" ++ str ntn ++ str "\" := " ++
+  str "\"" ++ str ntn ++ str "\" :=" ++ brk (1,2) ++
   prglob (Notation_ops.glob_constr_of_notation_constr c)
 
 let pr_notation_status on_parsing on_printing =
@@ -2007,7 +2007,7 @@ let pr_non_empty spc pp =
   if pp = mt () then mt () else spc ++ pp
 
 let pr_notation_data prglob (on_parsing,on_printing,{ not_interp  = (_, r); not_location = (_, df) }) =
-  hov 0 (pr_notation_info prglob df r ++ pr_non_empty (spc ()) (pr_notation_status on_parsing on_printing))
+  hov 0 (pr_notation_info prglob df r ++ pr_non_empty (brk(1,2)) (pr_notation_status on_parsing on_printing))
 
 let extract_notation_data (main,extra) =
   let main = match main with
@@ -2174,18 +2174,18 @@ let locate_notation prglob ntn scope =
   match ntns with
   | [] -> str "Unknown notation"
   | _ ->
-    str "Notation" ++ fnl () ++
     prlist_with_sep fnl (fun (ntn,l) ->
       let scope = find_default ntn scopes in
       prlist_with_sep fnl
         (fun (sc,(on_parsing,on_printing,{ not_interp  = (_, r); not_location = (_, df) })) ->
           hov 0 (
+            str "Notation" ++ brk (1,2) ++
             pr_notation_info prglob df r ++
             (if String.equal sc default_scope then mt ()
-             else (spc () ++ str ": " ++ str sc)) ++
+             else (brk (1,2) ++ str ": " ++ str sc)) ++
             (if Option.equal String.equal (Some sc) scope
-             then spc () ++ str "(default interpretation)" else mt ()) ++
-            pr_non_empty (spc ()) (pr_notation_status on_parsing on_printing)))
+             then brk (1,2) ++ str "(default interpretation)" else mt ()) ++
+            pr_non_empty (brk (1,2)) (pr_notation_status on_parsing on_printing)))
         l) ntns
 
 let collect_notation_in_scope scope sc known =
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index abada44da7..bd22d45059 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -231,16 +231,13 @@ fun l : list nat => match l with
      : list nat -> list nat
 
 Arguments foo _%list_scope
-Notation
-"'exists' x .. y , p" := ex (fun x => .. (ex (fun y => p)) ..) : type_scope
-(default interpretation)
-"'exists' ! x .. y , p" := ex
-                             (unique
-                                (fun x => .. (ex (unique (fun y => p))) ..))
-: type_scope (default interpretation)
-Notation
-"( x , y , .. , z )" := pair .. (pair x y) .. z : core_scope
-(default interpretation)
+Notation "'exists' x .. y , p" := (ex (fun x => .. (ex (fun y => p)) ..))
+  : type_scope (default interpretation)
+Notation "'exists' ! x .. y , p" :=
+  (ex (unique (fun x => .. (ex (unique (fun y => p))) ..))) : type_scope
+  (default interpretation)
+Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope
+  (default interpretation)
 1 subgoal
   
   ============================
diff --git a/test-suite/output/bug_9180.out b/test-suite/output/bug_9180.out
index ed4892b389..f035d0252a 100644
--- a/test-suite/output/bug_9180.out
+++ b/test-suite/output/bug_9180.out
@@ -1,4 +1,3 @@
-Notation
-"n .+1" := S n : nat_scope (default interpretation)
+Notation "n .+1" := (S n) : nat_scope (default interpretation)
 forall x : nat, x.+1 = x.+1
      : Prop
diff --git a/test-suite/output/locate.out b/test-suite/output/locate.out
index 473db2d312..93d9d6cf7b 100644
--- a/test-suite/output/locate.out
+++ b/test-suite/output/locate.out
@@ -1,3 +1,2 @@
-Notation
-"b1 && b2" := if b1 then b2 else false (default interpretation)
-"x && y" := andb x y : bool_scope
+Notation "b1 && b2" := (if b1 then b2 else false) (default interpretation)
+Notation "x && y" := (andb x y) : bool_scope