diff --git a/Source/DafnyLanguageServer/Workspace/ProjectManager.cs b/Source/DafnyLanguageServer/Workspace/ProjectManager.cs index 337e00bd790..efb56056c4c 100644 --- a/Source/DafnyLanguageServer/Workspace/ProjectManager.cs +++ b/Source/DafnyLanguageServer/Workspace/ProjectManager.cs @@ -1,4 +1,5 @@ using System; +using System.Collections.Concurrent; using System.Collections.Generic; using System.Collections.Immutable; using System.CommandLine; @@ -65,7 +66,7 @@ public class ProjectManager : IDisposable { /// private int version; - private int openFileCount; + private ConcurrentDictionary openFiles = new(); private VerifyOnMode AutomaticVerificationMode => options.Get(Verification); @@ -234,8 +235,8 @@ public void Save(TextDocumentIdentifier documentId) { /// Needs to be thread-safe /// /// - public bool CloseDocument() { - if (Interlocked.Decrement(ref openFileCount) == 0) { + public bool CloseDocument(Uri uri) { + if (openFiles.TryRemove(uri, out _) && openFiles.IsEmpty) { CloseAsync(); return true; } @@ -345,7 +346,7 @@ IntervalTree GetTree(Uri uri) { } public void OpenDocument(Uri uri, bool triggerCompilation) { - Interlocked.Increment(ref openFileCount); + openFiles.TryAdd(uri, 1); if (triggerCompilation) { StartNewCompilation(); diff --git a/Source/DafnyLanguageServer/Workspace/ProjectManagerDatabase.cs b/Source/DafnyLanguageServer/Workspace/ProjectManagerDatabase.cs index 513f666daad..3f93daa5984 100644 --- a/Source/DafnyLanguageServer/Workspace/ProjectManagerDatabase.cs +++ b/Source/DafnyLanguageServer/Workspace/ProjectManagerDatabase.cs @@ -76,7 +76,7 @@ public void CloseDocument(TextDocumentIdentifier documentId) { return; } - if (manager.CloseDocument()) { + if (manager.CloseDocument(documentId.Uri.ToUri())) { managersByProject.Remove(manager.Project.Uri, out _); } } @@ -139,7 +139,7 @@ public void CloseDocument(TextDocumentIdentifier documentId) { projectManagerForFile.CloseAsync(); managersByProject.Remove(project.Uri); } else { - var previousProjectHasNoDocuments = projectManagerForFile.CloseDocument(); + var previousProjectHasNoDocuments = projectManagerForFile.CloseDocument(projectManagerForFile.Project.Uri); if (previousProjectHasNoDocuments) { // Enable garbage collection managersByProject.Remove(projectManagerForFile.Project.Uri); diff --git a/docs/dev/news/4833.fix b/docs/dev/news/4833.fix new file mode 100644 index 00000000000..557bf88202f --- /dev/null +++ b/docs/dev/news/4833.fix @@ -0,0 +1 @@ +Removed one cause of need for restarting the IDE. \ No newline at end of file