From c3d2e50718bcb53e0a368209d2441d8b7c797f42 Mon Sep 17 00:00:00 2001
From: Jay Bosamiya <jayb@microsoft.com>
Date: Fri, 5 Jul 2024 14:54:18 -0700
Subject: [PATCH] wip

---
 src/lib.rs                 | 12 +++++++-----
 src/verus.pest             |  6 +++++-
 tests/verus-consistency.rs | 16 +++++++++++++++-
 3 files changed, 27 insertions(+), 7 deletions(-)

diff --git a/src/lib.rs b/src/lib.rs
index 34eb7d5..01da399 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -1603,7 +1603,7 @@ fn parse_and_format(s: &str) -> miette::Result<String> {
         match rule {
             Rule::non_verus | Rule::COMMENT => {
                 formatted_output += pair.as_str();
-                if matches!(pair.as_rule(), Rule::COMMENT) && is_multiline_comment(&pair) {
+                if matches!(pair.as_rule(), Rule::COMMENT) {
                     formatted_output += "\n";
                 }
             }
@@ -1625,12 +1625,8 @@ fn parse_and_format(s: &str) -> miette::Result<String> {
                     (prefix_comments, body, suffix_comments)
                 };
                 formatted_output += VERUS_PREFIX;
-                let mut final_prefix_comment_is_multiline = false;
                 for comment in &prefix_comments {
                     formatted_output += comment.as_str();
-                    final_prefix_comment_is_multiline = is_multiline_comment(comment);
-                }
-                if !prefix_comments.is_empty() && final_prefix_comment_is_multiline {
                     formatted_output += "\n";
                 }
 
@@ -1639,7 +1635,13 @@ fn parse_and_format(s: &str) -> miette::Result<String> {
                 if !suffix_comments.is_empty() {
                     formatted_output += "\n";
                 }
+                let mut first = true;
                 for comment in suffix_comments {
+                    if !first {
+                        formatted_output += "\n";
+                    } else {
+                        first = false;
+                    }
                     formatted_output += comment.as_str();
                 }
                 formatted_output += VERUS_SUFFIX;
diff --git a/src/verus.pest b/src/verus.pest
index 9bc3b3b..c97b39d 100644
--- a/src/verus.pest
+++ b/src/verus.pest
@@ -947,7 +947,11 @@ broadcast_use_list = {
 }
 
 broadcast_uses = {
-    broadcast_use+
+    // We explicitly eat up the extra WHITESPACEs here
+    // to prevent it from messing with the MULTI_NEWLINE
+    // handling, which would otherwise cause extra newlines
+    // to show up.
+    broadcast_use+ ~ WHITESPACE*
 }
 
 broadcast_use = {
diff --git a/tests/verus-consistency.rs b/tests/verus-consistency.rs
index 7442016..8c1c7dc 100644
--- a/tests/verus-consistency.rs
+++ b/tests/verus-consistency.rs
@@ -383,6 +383,7 @@ pub fn test() {
 
     pub fn test() {
         let Some((key, val)) = cur else { panic!()  /* covered by while condition */  };
+
         let Some((key, val)) = cur else { panic!() };
     }
 
@@ -782,7 +783,6 @@ fn len<T>(l: List<T>) -> nat {
             _ => false,
         }
     }
-
 }
 
 }
@@ -2424,5 +2424,19 @@ fn fff() {
 "#;
 
     assert_snapshot!(parse_and_format(file).unwrap(), @r###"
+    verus! {
+
+    fn fff() {
+        reveal(f1);  // reveal f1's definition just inside this block
+
+        reveal(f1);  // reveal f1's definition just inside this block
+
+        foo;
+
+        bar;
+        baz;
+    }
+
+    } // verus!
     "###);
 }