Fix formatting of var by statements

Source/DafnyCore/AST/Statements/BlockByProofStmt.cs

@@ -4,7 +4,8 @@
 
 namespace Microsoft.Dafny;
 
-public class BlockByProofStmt : Statement, ICanResolveNewAndOld, ICanPrint, ICloneable<Statement> {
+public class BlockByProofStmt : Statement, ICanResolveNewAndOld, ICanPrint,
+  ICloneable<Statement>, ICanFormat {
 
   public Statement Body { get; }
   public BlockStmt Proof { get; }
@@ -59,4 +60,10 @@ public override void ResolveGhostness(ModuleResolver resolver, ErrorReporter rep
 
     Proof.ResolveGhostness(resolver, reporter, true, codeContext, "a by block", allowAssumptionVariables, inConstructorInitializationPhase);
   }
+
+  public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) {
+    formatter.SetStatementIndentation(Body);
+    Proof.SetIndent(indentBefore, formatter);
+    return false;
+  }
 }

Source/DafnyCore/AST/Statements/BlockStmt.cs

@@ -61,12 +61,12 @@ public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) {
       }
     }
 
-    foreach (var blockStmtBody in Body) {
-      if (blockStmtBody is not BlockStmt && OwnedTokens.Any()) {
-        formatter.SetIndentations(blockStmtBody.StartToken, innerBlockIndent, innerBlockIndent);
+    foreach (var childStatement in Body) {
+      if (childStatement is not BlockStmt or BlockByProofStmt && OwnedTokens.Any()) {
+        formatter.SetIndentations(childStatement.StartToken, innerBlockIndent, innerBlockIndent);
       }
 
-      formatter.Visit(blockStmtBody, indentBefore + formatter.SpaceTab);
+      formatter.Visit(childStatement, indentBefore + formatter.SpaceTab);
     }
 
     return false;

Source/DafnyPipeline.Test/FormatterForStatements.cs

@@ -232,6 +232,32 @@ modify ... {
 ");
   }
 
+  [Fact]
+  public async Task FormatterWorksForReveal() {
+    await FormatterWorksFor(@"
+method Foo() {
+  var x := 3 by {
+    reveal p.q;
+  }
+  x := 4 by {
+    reveal p.q;
+  }
+  match foo {
+    case Some(x) => {
+      reveal x.y;
+      a := b(
+        c,
+        d 
+      );
+    }
+    case None => {
+      a := e;
+    }
+  }
+}
+");
+  }
+
   [Fact]
   public async Task FormatterWorksForDividedBlockStmt() {
     await FormatterWorksFor(@"

docs/dev/news/5927.fix

@@ -0,0 +1 @@
+Fix formatting of var by statements