Improve handling of separated clauses

Specifically, in the presence of comments around `expr_with_block`
cases (such as `assert ... by { ... }` blocks) that don't necessarily
have a semicolon, the previous version would end up reorganizing the
affinity of the comments across the clauses, preferring the previous
clause. With this commit, each comments stays loyal to its own clause.

CHANGELOG.md

@@ -1,5 +1,8 @@
 # Unreleased
 
+* Improved handling of comments around clauses/stanzas
+  - Each comment now maintains loyalty to the clause the user picked it to stay with, rather than automatically migrating to the previous clause in the presence of `assert ... by { ... }`-style constructs
+
 # v0.4.1
 
 * Minor fix to prevent panic on formatting files containing unbalanced parentheses in strings/chars/...

src/verus.pest

@@ -988,7 +988,11 @@ stmt = !{
   | proof_block
   | let_stmt
   | assignment_stmt
-  | expr_with_block ~ semi_str?
+  // We can't use `expr_with_block ~ semi_str?` here, and instead need to do it
+  // as the two separate ordered alternatives (`ewb ~ semi_str | ewb`) to
+  // prevent munching of multi-newlines that happens otherwise
+  | expr_with_block ~ semi_str
+  | expr_with_block
   | expr ~ semi_str
   | item_no_macro_call
   | macro_call_stmt

tests/verus-consistency.rs

@@ -2453,6 +2453,36 @@ fn fff() {
     baz;
 }
 
+pub fn foo() {
+    // this should stay stuck to the `a`
+    assert(a) by {
+        // whatever
+    }
+    // this should also stay stuck to the `a`
+    // and so should this line
+
+    // but this line
+    // and this line should stick to the `b`
+    b;
+    // and this comment should also stick to the `b`
+
+    // similarly `c`
+    c;
+    // `c` again
+
+    // and an empty comment stands alone
+
+    // similarly `d`
+    d;
+    // `d` again
+
+    // and finally, `d`
+    assert(d) by {
+        // whatever
+    }
+    // well, now done with `d`
+}
+
 } // verus!
 "#;
 
@@ -2470,6 +2500,36 @@ fn fff() {
         baz;
     }
 
+    pub fn foo() {
+        // this should stay stuck to the `a`
+        assert(a) by {
+            // whatever
+        }
+        // this should also stay stuck to the `a`
+        // and so should this line
+
+        // but this line
+        // and this line should stick to the `b`
+        b;
+        // and this comment should also stick to the `b`
+
+        // similarly `c`
+        c;
+        // `c` again
+
+        // and an empty comment stands alone
+
+        // similarly `d`
+        d;
+        // `d` again
+
+        // and finally, `d`
+        assert(d) by {
+            // whatever
+        }
+        // well, now done with `d`
+    }
+
     } // verus!
     "###);
 }