Skip to content

Commit d94af38

Browse files
authored
Fix: Formatting issue in forall statement range (#3961)
This PR fixes #3960 I added the corresponding test.. <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
1 parent a2159ca commit d94af38

File tree

3 files changed

+19
-0
lines changed

3 files changed

+19
-0
lines changed

Source/DafnyCore/AST/Statements/ForallStmt.cs

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -143,6 +143,9 @@ public List<BoundVar> UncompilableBoundVars() {
143143

144144
public bool SetIndent(int indentBefore, TokenNewIndentCollector formatter) {
145145
formatter.SetIndentLikeLoop(OwnedTokens, Body, indentBefore);
146+
if (Range != null) {
147+
formatter.Visit(Range, indentBefore + formatter.SpaceTab);
148+
}
146149
foreach (var ens in Ens) {
147150
formatter.SetAttributedExpressionIndentation(ens, indentBefore + formatter.SpaceTab);
148151
}

Source/DafnyPipeline.Test/FormatterIssues.cs

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4,6 +4,21 @@ namespace DafnyPipeline.Test;
44

55
[Collection("Singleton Test Collection - FormatterForTopLevelDeclarations")]
66
public class FormatterIssues : FormatterBaseTest {
7+
[Fact]
8+
public void GitIssue3960FormattingIssueForallStatements() {
9+
FormatterWorksFor(@"
10+
lemma Lemma()
11+
{
12+
forall pd0: int
13+
| && true
14+
&& (true
15+
&& true)
16+
&& true
17+
ensures true {
18+
}
19+
}");
20+
}
21+
722
[Fact]
823
public void GitIssue3944FormatterArgumentsDefaultValue() {
924
FormatterWorksFor(@"

docs/dev/news/3960.fix

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
Formatting issue in forall statement range

0 commit comments

Comments
 (0)