Improve formatting of record_pat

examples/syntax.rs

@@ -556,7 +556,7 @@ enum ThisOrThat {
 proof fn uses_is(t: ThisOrThat) {
     match t {
         ThisOrThat::This(..) => assert(t is This),
-        ThisOrThat::That{..} => assert(t is That),
+        ThisOrThat::That { .. } => assert(t is That),
     }
 }
 

examples/wip.rs

@@ -1,7 +1,7 @@
 verus! {
 
 fn test() {
-    for CKeyKV in v {
+    for CKeyKV { k, v } in v {
         res.insert(k, v);
     }
 }

src/lib.rs

@@ -896,8 +896,13 @@ fn to_doc<'a>(
         //Rule::wildcard_pat => arena.text("_"),
         Rule::end_only_range_pat => map_to_doc(ctx, arena, pair),
         Rule::ref_pat => arena.text("&").append(map_to_doc(ctx, arena, pair)),
-        Rule::record_pat => map_to_doc(ctx, arena, pair),
-        Rule::record_pat_field_list => comma_delimited(ctx, arena, pair).braces().group(),
+        Rule::record_pat => arena.concat(pair.into_inner().map(|p| match p.as_rule() {
+            Rule::path => to_doc(ctx, p, arena).append(arena.text(" ")),
+            _ => to_doc(ctx, p, arena),
+        })),
+        Rule::record_pat_field_list => {
+            spaced_braces(arena, comma_delimited(ctx, arena, pair)).group()
+        }
         Rule::record_pat_field => map_to_doc(ctx, arena, pair),
         Rule::tuple_struct_pat_inner => comma_delimited(ctx, arena, pair).parens().group(),
         Rule::tuple_struct_pat => map_to_doc(ctx, arena, pair),

tests/rustfmt-tests.rs

@@ -218,6 +218,14 @@ fn len<T>(l: List<T>) -> nat {
         List::Cons(_, tl) => 1 + len(*tl),
     }
 }
+
+fn uses_is(t: ThisOrThat) {
+     match t {
+        ThisOrThat::This(..) => assert(t),
+        ThisOrThat::That{..} => assert(t),
+     }
+}
+
 "#;
     compare(file);
 }
@@ -378,6 +386,13 @@ fn test() {
         res.insert(k, v);
     }
 }
+
+fn test() {
+    for CKeyKV { k, v } in v {
+        res.insert(k, v);
+    }
+}
+
 "#;
     compare(file);
 }