Closes #13142 (more standardized pretty-printing of records).

5 files changed, 114 insertions, 20 deletions

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 267f5e0b5f..14e734f1da 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -234,6 +234,42 @@ let tag_var = tag Tag.variable
             let f (id,c) = pr_id id ++ str ":=" ++ pr ltop c in
             str"@{" ++ hov 0 (prlist_with_sep pr_semicolon f (List.rev l)) ++ str"}"))
 
+  (* Assuming "{" and "}" brackets, prints
+     - if there is enough room
+       { a; b; c }
+     - otherwise
+       {
+        a;
+        b;
+        c
+       }
+    Alternatively, replace outer hv with h to get instead:
+       { a;
+         b;
+         c }
+    Replace the inner hv with hov to respectively get instead (if enough room):
+       {
+        a; b;
+        c
+       }
+    or
+       { a; b;
+         c }
+  *)
+  let pr_record left right pr = function
+    | [] -> str left ++ str " " ++ str right
+    | l ->
+      hv 0 (
+        str left ++
+        brk (1,String.length left) ++
+        hv 0 (prlist_with_sep pr_semicolon pr l) ++
+        brk (1,0) ++
+        str right)
+
+  let pr_record_body left right pr l =
+    let pr_defined_field (id, c) = hov 2 (pr_reference id ++ str" :=" ++ pr c) in
+    pr_record left right pr_defined_field l
+
   let las = lapp
   let lpator = 0
   let lpatrec = 0
@@ -242,11 +278,7 @@ let tag_var = tag Tag.variable
   let rec pr_patt sep inh p =
     let (strm,prec) = match CAst.(p.v) with
       | CPatRecord l ->
-        let pp (c, p) =
-          pr_reference c ++ spc() ++ str ":=" ++ pr_patt spc lpattop p
-        in
-        (if l = [] then str "{| |}"
-         else str "{| " ++ prlist_with_sep pr_semicolon pp l ++ str " |}"), lpatrec
+        pr_record_body "{|" "|}" (pr_patt spc lpattop) l, lpatrec
 
       | CPatAlias (p, na) ->
         pr_patt mt (LevelLe las) p ++ str " as " ++ pr_lname na, las
@@ -287,6 +319,7 @@ let tag_var = tag Tag.variable
 
       | CPatDelimiters (k,p) ->
         pr_delimiters k (pr_patt mt lsimplepatt p), 1
+
       | CPatCast _ ->
         assert false
     in
@@ -464,11 +497,6 @@ let tag_var = tag Tag.variable
       pr (LevelLt lapp) a  ++
         prlist (fun a -> spc () ++ pr_expl_args pr a) l)
 
-  let pr_record_body_gen pr l =
-    spc () ++
-    prlist_with_sep pr_semicolon
-      (fun (id, c) -> pr_reference id ++ str" :=" ++ pr ltop c) l
-
   let pr_forall n = keyword "forall" ++ pr_com_at n ++ spc ()
 
   let pr_fun n = keyword "fun" ++ pr_com_at n ++ spc ()
@@ -568,10 +596,7 @@ let tag_var = tag Tag.variable
       | CApp ((None,a),l) ->
         return (pr_app (pr mt) a l, lapp)
       | CRecord l ->
-        return (
-          hv 0 (str"{|" ++ pr_record_body_gen (pr spc) l ++ str" |}"),
-          latom
-        )
+        return (pr_record_body "{|" "|}" (pr spc ltop) l, latom)
       | CCases (Constr.LetPatternStyle,rtntypopt,[c,as_clause,in_clause],[{v=([[p]],b)}]) ->
         return (
           hv 0 (
@@ -717,7 +742,5 @@ let tag_var = tag Tag.variable
 
   let pr_cases_pattern_expr = pr_patt ltop
 
-  let pr_record_body = pr_record_body_gen pr
-
   let pr_binders env sigma = pr_undelimited_binders spc (pr_expr env sigma ltop)
 
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index 2850e4bfa0..02e04573f8 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -41,7 +41,8 @@ val pr_guard_annot
   -> recursion_order_expr option
   -> Pp.t
 
-val pr_record_body : (qualid * constr_expr) list -> Pp.t
+val pr_record : string -> string -> ('a -> Pp.t) -> 'a list -> Pp.t
+val pr_record_body : string -> string -> ('a -> Pp.t) -> (Libnames.qualid * 'a) list -> Pp.t
 val pr_binders : Environ.env -> Evd.evar_map -> local_binder_expr list -> Pp.t
 val pr_constr_pattern_expr : Environ.env -> Evd.evar_map -> constr_pattern_expr -> Pp.t
 val pr_lconstr_pattern_expr : Environ.env -> Evd.evar_map -> constr_pattern_expr -> Pp.t
diff --git a/test-suite/output/Record.out b/test-suite/output/Record.out
index d45343fe60..7de1e7d559 100644
--- a/test-suite/output/Record.out
+++ b/test-suite/output/Record.out
@@ -30,3 +30,43 @@ fun '{| U := T; a := a; q := p |} => (T, p, a)
      : M -> Type * True * nat
 fun '{| U := T; a := a; q := p |} => (T, p, a)
      : M -> Type * True * nat
+{| a := 0; b := 0 |}
+     : T
+fun '{| |} => 0
+     : LongModuleName.test -> nat
+     = {|
+         a :=
+           {|
+             LongModuleName.long_field_name0 := 0;
+             LongModuleName.long_field_name1 := 1;
+             LongModuleName.long_field_name2 := 2;
+             LongModuleName.long_field_name3 := 3
+           |};
+         b :=
+           fun
+             '{|
+                LongModuleName.long_field_name0 := a;
+                LongModuleName.long_field_name1 := b;
+                LongModuleName.long_field_name2 := c;
+                LongModuleName.long_field_name3 := d
+              |} => (a, b, c, d)
+       |}
+     : T
+     = {|
+         a :=
+           {|
+             long_field_name0 := 0;
+             long_field_name1 := 1;
+             long_field_name2 := 2;
+             long_field_name3 := 3
+           |};
+         b :=
+           fun
+             '{|
+                long_field_name0 := a;
+                long_field_name1 := b;
+                long_field_name2 := c;
+                long_field_name3 := d
+              |} => (a, b, c, d)
+       |}
+     : T
diff --git a/test-suite/output/Record.v b/test-suite/output/Record.v
index 71a8afa131..13ea37b11e 100644
--- a/test-suite/output/Record.v
+++ b/test-suite/output/Record.v
@@ -33,3 +33,34 @@ Check fun x:M => let 'D T _ p := x in T.
 Check fun x:M => let 'D T p := x in (T,p).
 Check fun x:M => let 'D T a p := x in (T,p,a).
 Check fun x:M => let '{|U:=T;a:=a;q:=p|} := x in (T,p,a).
+
+Module FormattingIssue13142.
+
+Record T {A B} := {a:A;b:B}.
+
+Module LongModuleName.
+  Record test := { long_field_name0 : nat;
+                  long_field_name1 : nat;
+                  long_field_name2 : nat;
+                  long_field_name3 : nat }.
+End LongModuleName.
+
+Definition c :=
+      {| LongModuleName.long_field_name0 := 0;
+         LongModuleName.long_field_name1 := 1;
+         LongModuleName.long_field_name2 := 2;
+         LongModuleName.long_field_name3 := 3 |}.
+
+Definition d :=
+ fun '{| LongModuleName.long_field_name0 := a;
+         LongModuleName.long_field_name1 := b;
+         LongModuleName.long_field_name2 := c;
+         LongModuleName.long_field_name3 := d |} => (a,b,c,d).
+
+Check {|a:=0;b:=0|}.
+Check fun '{| LongModuleName.long_field_name0:=_ |} => 0.
+Eval compute in {|a:=c;b:=d|}.
+Import LongModuleName.
+Eval compute in {|a:=c;b:=d|}.
+
+End FormattingIssue13142.
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index f972e05d3b..e9cd4272e6 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -524,8 +524,7 @@ let pr_record_field (x, { rf_subclass = oc ; rf_priority = pri ; rf_notation = n
   prx ++ prpri ++ prlist (pr_decl_notation @@ pr_constr) ntn
 
 let pr_record_decl c fs =
-  pr_opt pr_lident c ++ (if c = None then str"{" else str" {") ++
-  hv 0 (prlist_with_sep pr_semicolon pr_record_field fs ++ str"}")
+  pr_opt pr_lident c ++ pr_record "{" "}" pr_record_field fs
 
 let pr_printable = function
   | PrintFullContext ->
@@ -966,7 +965,7 @@ let pr_vernac_expr v =
         str":" ++ spc () ++
         pr_constr cl ++ pr_hint_info pr_constr_pattern_expr info ++
         (match props with
-         | Some (true, { v = CRecord l}) -> spc () ++ str":=" ++ spc () ++ str"{" ++ pr_record_body l ++ str "}"
+         | Some (true, { v = CRecord l}) -> spc () ++ str":=" ++ spc () ++ pr_record_body "{" "}" pr_lconstr l
          | Some (true,_) -> assert false
          | Some (false,p) -> spc () ++ str":=" ++ spc () ++ pr_constr p
          | None -> mt()))