wip

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;

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 = {

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!
     "###);
 }