Handle trailing newlines for broadcast uses

CHANGELOG.md

@@ -1,6 +1,7 @@
 # Unreleased
 
 * Support attributes on `broadcast group` items
+* Improve styling of `broadcast use`s, ensuring trailing newline
 
 # v0.2.11
 

examples/verus-snapshot/source/vstd/source/vstd/seq_lib.rs

@@ -971,6 +971,7 @@ impl<A> Seq<Seq<A>> {
             self.len() == 1 ==> self.flatten() == self.first(),
     {
         broadcast use Seq::add_empty_right;
+
         if self.len() == 1 {
             assert(self.flatten() =~= self.first().add(self.drop_first().flatten()));
         }
@@ -1022,6 +1023,7 @@ impl<A> Seq<Seq<A>> {
         decreases self.len(),
     {
         broadcast use Seq::add_empty_right, Seq::push_distributes_over_add;
+
         if self.len() != 0 {
             self.drop_last().lemma_flatten_and_flatten_alt_are_equivalent();
             seq![self.last()].lemma_flatten_one_element();

src/lib.rs

@@ -394,8 +394,16 @@ fn items_to_doc<'a>(
             }
             prev_is_use = is_use;
 
+            let is_broadcast_uses = matches!(
+                item.clone().into_inner().next().unwrap().as_rule(),
+                Rule::broadcast_uses
+            );
             res = res.append(to_doc(ctx, item, arena));
-            res = res.append(arena.line());
+            if !is_broadcast_uses {
+                // Add the newline, but don't add extra newlines between `broadcast use`s since
+                // those already add newlines
+                res = res.append(arena.line());
+            }
             // Add extra space between items, except for use declarations
             if i < len - 1 && !is_use {
                 res = res.append(arena.line());
@@ -991,6 +999,14 @@ fn to_doc<'a>(
         Rule::attr_inner => map_to_doc(ctx, arena, pair),
         Rule::meta => unsupported(pair),
         Rule::broadcast_use => map_to_doc(ctx, arena, pair),
+        Rule::broadcast_uses => arena.concat(pair.into_inner().map(|p| {
+            if matches!(p.as_rule(), Rule::broadcast_use) {
+                to_doc(ctx, p, arena).append(arena.hardline())
+            } else {
+                // Handle the comments
+                to_doc(ctx, p, arena)
+            }
+        })),
         Rule::broadcast_group => map_to_doc(ctx, arena, pair),
 
         //****************************//

src/verus.pest

@@ -590,7 +590,7 @@ item_no_macro_call = _{
   | union
   | use
   | broadcast_group
-  | broadcast_use
+  | broadcast_uses
 }
 
 verusfmt_skipped_item = {
@@ -903,6 +903,10 @@ broadcast_use_list = {
     (path ~ ("," ~ path)* ~ ","?)
 }
 
+broadcast_uses = {
+    broadcast_use+
+}
+
 broadcast_use = {
     broadcast_str ~ use_str ~ broadcast_use_list ~ semi_str
 }

tests/verus-consistency.rs

@@ -1990,6 +1990,7 @@ mod m4 {
                 p.inv(),
         {
             broadcast use Ring::properties;
+
             assert(p.spec_succ().spec_prev() == p);
             assert(p.spec_prev().spec_succ() == p);
         }
@@ -2018,3 +2019,46 @@ mod m4 {
     } // verus!
     "###);
 }
+
+#[test]
+fn verus_broadcast_uses_trailing_newline() {
+    let file = r###"
+verus! {
+proof fn to_multiset_build<A>(s: Seq<A>, a: A)
+    ensures
+        s.push(a).to_multiset() =~= s.to_multiset().insert(a),
+    decreases s.len(),
+{
+    broadcast use crate::multiset::multiset_axioms;
+    /* xx */
+    broadcast use crate::multiset::multiset_stuffs;
+    // xx
+    broadcast use crate::useful;
+    broadcast use crate::moreuseful;
+    if s.len() == 0 {
+    }
+}
+} // verus!
+"###;
+    assert_snapshot!(parse_and_format(file).unwrap(), @r###"
+    verus! {
+
+    proof fn to_multiset_build<A>(s: Seq<A>, a: A)
+        ensures
+            s.push(a).to_multiset() =~= s.to_multiset().insert(a),
+        decreases s.len(),
+    {
+        broadcast use crate::multiset::multiset_axioms;
+        /* xx */
+        broadcast use crate::multiset::multiset_stuffs;
+        // xx
+        broadcast use crate::useful;
+        broadcast use crate::moreuseful;
+
+        if s.len() == 0 {
+        }
+    }
+
+    } // verus!
+    "###);
+}