Fix syn parsing's continue_parsing_early for assert/proof

verus-lang · Feb 6, 2025 · 5e8df04 · 5e8df04
1 parent 8e7820d
commit 5e8df04
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 2 deletions.
diff --git a/dependencies/syn/src/classify.rs b/dependencies/syn/src/classify.rs
@@ -34,8 +34,8 @@ pub(crate) fn requires_comma_to_be_match_arm(expr: &Expr) -> bool {
         | Expr::Const(_) => false,
 
         // verus
-        | Expr::Assert(e) => e.body.is_none(),
-        | Expr::AssertForall(_) => false,
+        Expr::Assert(e) => e.body.is_none(),
+        Expr::AssertForall(_) => false,
         Expr::Assume(_)
         | Expr::RevealHide(_)
         | Expr::View(_)

diff --git a/dependencies/syn/src/expr.rs b/dependencies/syn/src/expr.rs
@@ -2313,6 +2313,12 @@ pub(crate) mod parsing {
             | Expr::Unsafe(_)
             | Expr::Const(_)
             | Expr::Block(_) => false,
+
+            // verus
+            Expr::Assert(e) => e.body.is_none(),
+            Expr::AssertForall(_) => false,
+            Expr::Unary(e) if matches!(e.op, crate::op::UnOp::Proof(_)) => false,
+
             _ => true,
         }
     }