Fix: Formatting on VSCode for multi-file projects with project file

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 
   /// </summary>
-  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) {

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;
     }

Source/DafnyDriver/Commands/FormatCommand.cs

@@ -86,7 +86,7 @@ public static async Task<ExitValue> 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) {

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) {

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");