From 29982961bf2e48317c246d98674d4a21c75405c2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= Date: Mon, 8 Jan 2024 07:31:46 -0600 Subject: [PATCH] Fix: Formatting on VSCode for multi-file projects with project file (#4918) I fixed the fact that the formatter was trying to incorporate every file in the DafnyFile project instead of considering only the file being viewed. I also updated the tests to reflect this new parameter. I tested manually, and when formatting a file part of a project file, the formatting now works seamlessly (fixes https://github.com/dafny-lang/dafny/issues/4836) 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). --- Source/DafnyCore/AST/Grammar/IndentationFormatter.cs | 8 ++++++-- Source/DafnyCore/AST/Grammar/TokenNewIndentCollector.cs | 6 ++++-- Source/DafnyDriver/Commands/FormatCommand.cs | 2 +- Source/DafnyLanguageServer/Workspace/Compilation.cs | 2 +- Source/DafnyPipeline.Test/FormatterBaseTest.cs | 8 ++++---- 5 files changed, 16 insertions(+), 10 deletions(-) diff --git a/Source/DafnyCore/AST/Grammar/IndentationFormatter.cs b/Source/DafnyCore/AST/Grammar/IndentationFormatter.cs index 0256db2fb2..e2e83a3a0a 100644 --- a/Source/DafnyCore/AST/Grammar/IndentationFormatter.cs +++ b/Source/DafnyCore/AST/Grammar/IndentationFormatter.cs @@ -23,11 +23,15 @@ public IndentationFormatter(TokenNewIndentCollector formatter) { /// Creates an IndentationFormatter for the given program, /// by immediately processing all nodes and assigning indentations to most structural tokens /// - public static IndentationFormatter ForProgram(Program program, bool reduceBlockiness = true) { - var tokenNewIndentCollector = new TokenNewIndentCollector(program) { + public static IndentationFormatter ForProgram(Program program, Uri fileToFormat, bool reduceBlockiness = true) { + var tokenNewIndentCollector = new TokenNewIndentCollector(program, fileToFormat) { ReduceBlockiness = reduceBlockiness }; foreach (var child in program.DefaultModuleDef.PreResolveChildren) { + var isPhysicalToken = child.Tok.line != 0; + if (isPhysicalToken && child.Tok.Uri != fileToFormat) { + continue; + } if (child is TopLevelDecl topLevelDecl) { tokenNewIndentCollector.SetDeclIndentation(topLevelDecl, 0); } else if (child is Include include) { diff --git a/Source/DafnyCore/AST/Grammar/TokenNewIndentCollector.cs b/Source/DafnyCore/AST/Grammar/TokenNewIndentCollector.cs index ca0597ec55..0a2c218065 100644 --- a/Source/DafnyCore/AST/Grammar/TokenNewIndentCollector.cs +++ b/Source/DafnyCore/AST/Grammar/TokenNewIndentCollector.cs @@ -83,8 +83,9 @@ private Indentations PosToIndentations(int pos) { public int binOpIndent = -1; public int binOpArgIndent = -1; - internal TokenNewIndentCollector(Program program) { + internal TokenNewIndentCollector(Program program, Uri fileToFormat) { this.program = program; + this.fileToFormat = fileToFormat; preResolve = true; } @@ -222,6 +223,7 @@ public int GetRightAlignIndentAfter(IToken token, int indentFallback) { } private static readonly Regex FollowedByNewlineRegex = new Regex("^[ \t]*([\r\n]|//)"); + private readonly Uri fileToFormat; public static bool IsFollowedByNewline(IToken token) { return FollowedByNewlineRegex.IsMatch(token.TrailingTrivia); @@ -231,7 +233,7 @@ public static bool IsFollowedByNewline(IToken token) { // 'inline' is the hypothetical indentation of this token if it was on its own line // 'below' is the hypothetical indentation of a comment after that token, and of the next token if it does not have a set indentation public void SetIndentations(IToken token, int above = -1, int inline = -1, int below = -1) { - if (token.FromIncludeDirective(program) || (token.line == 0 && token.col == 0)) { + if (token.Uri != fileToFormat || (token.line == 0 && token.col == 0)) { // Just ignore this token. return; } diff --git a/Source/DafnyDriver/Commands/FormatCommand.cs b/Source/DafnyDriver/Commands/FormatCommand.cs index 130f69a702..7782a1aa78 100644 --- a/Source/DafnyDriver/Commands/FormatCommand.cs +++ b/Source/DafnyDriver/Commands/FormatCommand.cs @@ -86,7 +86,7 @@ public static async Task DoFormatting(DafnyOptions options) { var result = originalText; if (firstToken != null) { result = Formatting.__default.ReindentProgramFromFirstToken(firstToken, - IndentationFormatter.ForProgram(dafnyProgram)); + IndentationFormatter.ForProgram(dafnyProgram, file.Uri)); if (result != originalText) { neededFormatting += 1; if (doCheck) { diff --git a/Source/DafnyLanguageServer/Workspace/Compilation.cs b/Source/DafnyLanguageServer/Workspace/Compilation.cs index 1749a61af1..50a14ccf99 100644 --- a/Source/DafnyLanguageServer/Workspace/Compilation.cs +++ b/Source/DafnyLanguageServer/Workspace/Compilation.cs @@ -428,7 +428,7 @@ public void CancelPendingUpdates() { firstToken = firstToken.Prev; } var result = Formatting.__default.ReindentProgramFromFirstToken(firstToken, - IndentationFormatter.ForProgram(program)); + IndentationFormatter.ForProgram(program, firstToken.Uri)); var lastToken = firstToken; while (lastToken.Next != null) { diff --git a/Source/DafnyPipeline.Test/FormatterBaseTest.cs b/Source/DafnyPipeline.Test/FormatterBaseTest.cs index 0e7aa59c25..ef393b30b4 100644 --- a/Source/DafnyPipeline.Test/FormatterBaseTest.cs +++ b/Source/DafnyPipeline.Test/FormatterBaseTest.cs @@ -75,7 +75,7 @@ protected void FormatterWorksFor(string testCase, string? expectedProgramString var reprinted = firstToken != null && firstToken.line > 0 ? Formatting.__default.ReindentProgramFromFirstToken(firstToken, - IndentationFormatter.ForProgram(dafnyProgram, reduceBlockiness)) + IndentationFormatter.ForProgram(dafnyProgram, firstToken.Uri, reduceBlockiness)) : programString; EnsureEveryTokenIsOwned(uri, programNotIndented, dafnyProgram); if (expectedProgram != reprinted) { @@ -100,7 +100,7 @@ protected void FormatterWorksFor(string testCase, string? expectedProgramString }); var reprintedCloned = firstToken != null && firstToken.line > 0 ? Formatting.__default.ReindentProgramFromFirstToken(firstToken, - IndentationFormatter.ForProgram(dafnyProgram, reduceBlockiness)) + IndentationFormatter.ForProgram(dafnyProgram, firstToken.Uri, reduceBlockiness)) : programString; EnsureEveryTokenIsOwned(uri, programNotIndented, dafnyProgram); if (expectedProgram != reprintedCloned) { @@ -112,7 +112,7 @@ protected void FormatterWorksFor(string testCase, string? expectedProgramString DafnyMain.Resolve(dafnyProgram); reprinted = firstToken != null && firstToken.line > 0 ? Formatting.__default.ReindentProgramFromFirstToken(firstToken, - IndentationFormatter.ForProgram(dafnyProgram, reduceBlockiness)) + IndentationFormatter.ForProgram(dafnyProgram, firstToken.Uri, reduceBlockiness)) : programString; if (expectedProgram != reprinted) { options.ErrorWriter.WriteLine("Formatting after resolution generates an error:"); @@ -131,7 +131,7 @@ protected void FormatterWorksFor(string testCase, string? expectedProgramString firstToken = dafnyProgram.GetFirstTokenForUri(uri); var reprinted2 = firstToken != null && firstToken.line > 0 ? Formatting.__default.ReindentProgramFromFirstToken(firstToken, - IndentationFormatter.ForProgram(dafnyProgram, reduceBlockiness)) + IndentationFormatter.ForProgram(dafnyProgram, firstToken.Uri, reduceBlockiness)) : reprinted; if (reprinted != reprinted2) { Console.Write("Double formatting is not stable:\n");