@@ -268,10 +268,29 @@ export class FileSystemProvider implements vscode.FileSystemProvider {
268268 private _bufferedEvents : vscode . FileChangeEvent [ ] = [ ] ;
269269 private _fireSoonHandle ?: NodeJS . Timeout ;
270270
271+ /**
272+ * The stringified URIs of all `isfs` documents that may have had
273+ * their contents changed during the last time they were saved
274+ */
275+ private readonly _needsUpdate : Set < string > = new Set ( ) ;
276+
271277 public constructor ( ) {
272278 this . onDidChangeFile = this . _emitter . event ;
273279 }
274280
281+ /**
282+ * Check if this `isfs` document stringified URI was changed during
283+ * the last time it was saved. This is used to force VS Code to update
284+ * the editor tab containing the file.
285+ */
286+ public needsUpdate ( uriString : string ) : boolean {
287+ if ( this . _needsUpdate . has ( uriString ) ) {
288+ this . _needsUpdate . delete ( uriString ) ;
289+ return true ;
290+ }
291+ return false ;
292+ }
293+
275294 // Used by import and compile to make sure we notice its changes
276295 public fireFileChanged ( uri : vscode . Uri ) : void {
277296 this . _fireSoon ( { type : vscode . FileChangeType . Changed , uri } ) ;
@@ -619,35 +638,14 @@ export class FileSystemProvider implements vscode.FileSystemProvider {
619638 return this . compile ( uri , entry , update ) ;
620639 } else if ( update ) {
621640 // The file's contents may have changed as a result of the save,
622- // so make sure we notify VS Code and any watchers of the change
623- this . _notifyOfFileChange ( uri ) ;
641+ // so make sure VS Code updates the editor tab contents if needed
642+ this . _needsUpdate . add ( uri . toString ( ) ) ;
624643 } else if ( ! created ) {
625644 this . _fireSoon ( { type : vscode . FileChangeType . Changed , uri } ) ;
626645 }
627646 } ) ;
628647 }
629648
630- /**
631- * Notify VS Code and any watchers that the contents of `uri` changed.
632- * Use this function instead of firing the file change event directly
633- * when we need to force the VS Code UI to show the change. For example,
634- * if the server changed the document during a save.
635- */
636- private _notifyOfFileChange ( uri : vscode . Uri ) : void {
637- // The file's contents may have changed as a result of the save,
638- // so make sure we notify VS Code and any watchers of the change
639- const uriString = uri . toString ( ) ;
640- if ( vscode . window . activeTextEditor ?. document . uri . toString ( ) == uriString ) {
641- setTimeout ( ( ) => {
642- const activeDoc = vscode . window . activeTextEditor ?. document ;
643- if ( activeDoc && ! activeDoc . isDirty && ! activeDoc . isClosed && activeDoc . uri . toString ( ) == uriString ) {
644- // Force VS Code to refresh the file's contents in the editor UI
645- vscode . commands . executeCommand ( "workbench.action.files.revert" ) ;
646- }
647- } , 75 ) ;
648- }
649- }
650-
651649 /** Process a Document object that was successfully deleted. */
652650 private async processDeletedDoc ( doc : Document , uri : vscode . Uri , csp : boolean , project : boolean ) : Promise < void > {
653651 const events : vscode . FileChangeEvent [ ] = [ ] ;
@@ -917,7 +915,7 @@ export class FileSystemProvider implements vscode.FileSystemProvider {
917915 if ( update || ( file && filesToUpdate . includes ( file . fileName ) ) ) {
918916 // This file was just written and the write may have changed its contents or the
919917 // compilation changed its contents. Therefore, we must force VS Code to update it.
920- this . _notifyOfFileChange ( uri ) ;
918+ this . _needsUpdate . add ( uri . toString ( ) ) ;
921919 }
922920 // Fire file changed events for all files changed by compilation
923921 this . _fireSoon (
0 commit comments