From 113282d99766cdfa29dccc6b4663210fbae199f7 Mon Sep 17 00:00:00 2001
From: Bryan Parno <parno@cmu.edu>
Date: Thu, 16 Nov 2023 14:28:42 -0500
Subject: [PATCH] Improve formatting of record_pat

---
 examples/syntax.rs     |  2 +-
 examples/wip.rs        |  2 +-
 src/lib.rs             |  9 +++++++--
 tests/rustfmt-tests.rs | 15 +++++++++++++++
 4 files changed, 24 insertions(+), 4 deletions(-)

diff --git a/examples/syntax.rs b/examples/syntax.rs
index 082a948..20536a8 100644
--- a/examples/syntax.rs
+++ b/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),
     }
 }
 
diff --git a/examples/wip.rs b/examples/wip.rs
index 3ad72a9..9bd6ce5 100644
--- a/examples/wip.rs
+++ b/examples/wip.rs
@@ -1,7 +1,7 @@
 verus! {
 
 fn test() {
-    for CKeyKV in v {
+    for CKeyKV { k, v } in v {
         res.insert(k, v);
     }
 }
diff --git a/src/lib.rs b/src/lib.rs
index 18124ce..dee65c1 100644
--- a/src/lib.rs
+++ b/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),
diff --git a/tests/rustfmt-tests.rs b/tests/rustfmt-tests.rs
index a5f260e..82512f5 100644
--- a/tests/rustfmt-tests.rs
+++ b/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);
 }