Fix automatic refresh of server-side documents after save and compile (#1678)

Author: isc-bsaviano

src/extension.ts

@@ -1897,6 +1897,20 @@ export async function activate(context: vscode.ExtensionContext): Promise<any> {
       sendCommandTelemetryEvent("showAllClassMembers");
       if (uri instanceof vscode.Uri) showAllClassMembers(uri);
     }),
+    vscode.workspace.onDidSaveTextDocument((d) => {
+      // If the document just saved is a server-side document that needs to be updated in the UI,
+      // then force VS Code to update the document's contents. This is needed if the document has
+      // been changed during a save, for example by adding or changing the Storage definition.
+      if (notIsfs(d.uri)) return;
+      const uriString = d.uri.toString();
+      if (fileSystemProvider.needsUpdate(uriString)) {
+        const activeDoc = vscode.window.activeTextEditor?.document;
+        if (activeDoc && !activeDoc.isDirty && !activeDoc.isClosed && activeDoc.uri.toString() == uriString) {
+          // Force VS Code to refresh the file's contents in the editor tab
+          vscode.commands.executeCommand("workbench.action.files.revert");
+        }
+      }
+    }),
     // These three listeners are needed to keep track of which file events were caused by VS Code
     // to support the "vscodeOnly" option for the objectscript.syncLocalChanges setting.
     // They store the URIs of files that are about to be changed by VS Code.

src/providers/FileSystemProvider/FileSystemProvider.ts

@@ -268,10 +268,29 @@ export class FileSystemProvider implements vscode.FileSystemProvider {
   private _bufferedEvents: vscode.FileChangeEvent[] = [];
   private _fireSoonHandle?: NodeJS.Timeout;
 
+  /**
+   * The stringified URIs of all `isfs` documents that may have had
+   * their contents changed during the last time they were saved
+   */
+  private readonly _needsUpdate: Set<string> = new Set();
+
   public constructor() {
     this.onDidChangeFile = this._emitter.event;
   }
 
+  /**
+   * Check if this `isfs` document stringified URI was changed during
+   * the last time it was saved. This is used to force VS Code to update
+   * the editor tab containing the file.
+   */
+  public needsUpdate(uriString: string): boolean {
+    if (this._needsUpdate.has(uriString)) {
+      this._needsUpdate.delete(uriString);
+      return true;
+    }
+    return false;
+  }
+
   // Used by import and compile to make sure we notice its changes
   public fireFileChanged(uri: vscode.Uri): void {
     this._fireSoon({ type: vscode.FileChangeType.Changed, uri });
@@ -476,6 +495,9 @@ export class FileSystemProvider implements vscode.FileSystemProvider {
       overwrite: boolean;
     }
   ): void | Thenable<void> {
+    const originalUriString = uri.toString();
+    const originalUri = vscode.Uri.parse(originalUriString);
+    this._needsUpdate.delete(originalUriString);
     uri = redirectDotvscodeRoot(uri, new vscode.FileSystemError("Server does not have a /_vscode web application"));
     if (uri.path.startsWith("/.")) {
       throw new vscode.FileSystemError("dot-folders are not supported by server");
@@ -616,38 +638,17 @@ export class FileSystemProvider implements vscode.FileSystemProvider {
           // is part of the "write" operation from VS Code's point of view. This is required
           // to prevent concurreny issues when VS Code refreshs its internal representaton of
           // the file system while documents are being compiled.
-          return this.compile(uri, entry, update);
+          return this.compile(originalUri, entry, update);
         } else if (update) {
           // The file's contents may have changed as a result of the save,
-          // so make sure we notify VS Code and any watchers of the change
-          this._notifyOfFileChange(uri);
+          // so make sure VS Code updates the editor tab contents if needed
+          this._needsUpdate.add(originalUriString);
         } else if (!created) {
-          this._fireSoon({ type: vscode.FileChangeType.Changed, uri });
+          this._fireSoon({ type: vscode.FileChangeType.Changed, uri: originalUri });
         }
       });
   }
 
-  /**
-   * Notify VS Code and any watchers that the contents of `uri` changed.
-   * Use this function instead of firing the file change event directly
-   * when we need to force the VS Code UI to show the change. For example,
-   * if the server changed the document during a save.
-   */
-  private _notifyOfFileChange(uri: vscode.Uri): void {
-    // The file's contents may have changed as a result of the save,
-    // so make sure we notify VS Code and any watchers of the change
-    const uriString = uri.toString();
-    if (vscode.window.activeTextEditor?.document.uri.toString() == uriString) {
-      setTimeout(() => {
-        const activeDoc = vscode.window.activeTextEditor?.document;
-        if (activeDoc && !activeDoc.isDirty && !activeDoc.isClosed && activeDoc.uri.toString() == uriString) {
-          // Force VS Code to refresh the file's contents in the editor UI
-          vscode.commands.executeCommand("workbench.action.files.revert");
-        }
-      }, 75);
-    }
-  }
-
   /** Process a Document object that was successfully deleted. */
   private async processDeletedDoc(doc: Document, uri: vscode.Uri, csp: boolean, project: boolean): Promise<void> {
     const events: vscode.FileChangeEvent[] = [];
@@ -867,6 +868,9 @@ export class FileSystemProvider implements vscode.FileSystemProvider {
    */
   public async compile(uri: vscode.Uri, file?: File, update?: boolean): Promise<void> {
     if (!uri || uri.scheme != FILESYSTEM_SCHEMA) return;
+    const originalUriString = uri.toString();
+    const originalUri = vscode.Uri.parse(originalUriString);
+    this._needsUpdate.delete(originalUriString);
     uri = redirectDotvscodeRoot(uri, new vscode.FileSystemError("Server does not have a /_vscode web application"));
     const compileList: string[] = [];
     try {
@@ -914,17 +918,36 @@ export class FileSystemProvider implements vscode.FileSystemProvider {
           })
           .catch(() => compileErrorMsg(conf))
     );
-    if (update || (file && filesToUpdate.includes(file.fileName))) {
+    if (file && (update || filesToUpdate.includes(file.fileName))) {
       // This file was just written and the write may have changed its contents or the
       // compilation changed its contents. Therefore, we must force VS Code to update it.
-      this._notifyOfFileChange(uri);
+      this._needsUpdate.add(originalUriString);
+    }
+    if (filesToUpdate.length) {
+      // Force VS Code to refresh the active editor tab's contents if the file was changed
+      // by compilation and is NOT the file that was saved if this is a post-save compilation
+      const activeDoc = vscode.window.activeTextEditor?.document;
+      if (activeDoc && !activeDoc.isDirty && !activeDoc.isClosed) {
+        const activeDocUriString = activeDoc.uri.toString();
+        if (
+          !(file && activeDocUriString == originalUriString) &&
+          filesToUpdate.some(
+            (f) =>
+              DocumentContentProvider.getUri(f, undefined, undefined, undefined, originalUri)?.toString() ==
+              activeDocUriString
+          )
+        ) {
+          // Force VS Code to refresh the contents in the active editor tab
+          vscode.commands.executeCommand("workbench.action.files.revert");
+        }
+      }
     }
     // Fire file changed events for all files changed by compilation
     this._fireSoon(
       ...filesToUpdate.map((f) => {
         return {
           type: vscode.FileChangeType.Changed,
-          uri: DocumentContentProvider.getUri(f, undefined, undefined, undefined, uri),
+          uri: DocumentContentProvider.getUri(f, undefined, undefined, undefined, originalUri),
         };
       })
     );
@@ -942,7 +965,7 @@ export class FileSystemProvider implements vscode.FileSystemProvider {
       ).map((f: string) => {
         return {
           type: vscode.FileChangeType.Changed,
-          uri: DocumentContentProvider.getUri(f, undefined, undefined, undefined, uri),
+          uri: DocumentContentProvider.getUri(f, undefined, undefined, undefined, originalUri),
         };
       })
     );