Skip to content

Commit

Permalink
Fix: No more spurious restart needed in the IDE (#4834)
Browse files Browse the repository at this point in the history
Fixes #4833 

### Description
I replaced the openFileCount by openFiles so that closing a document,
even if unexpected like VSCode does randomly, won't trigger the
Compilation object to be disposed, which crashes the IDE every 3-4
minutes on projects with multiple files open.

### How has this been tested?
I have been enjoying the IDE for 20 minutes straight without restarting
it. It's a fantastic experience. I'm going to turn on "verification on
change" again.

<small>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).</small>
  • Loading branch information
MikaelMayer authored Dec 1, 2023
1 parent 05f4710 commit 23a083b
Show file tree
Hide file tree
Showing 3 changed files with 8 additions and 6 deletions.
9 changes: 5 additions & 4 deletions Source/DafnyLanguageServer/Workspace/ProjectManager.cs
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
using System;
using System.Collections.Concurrent;
using System.Collections.Generic;
using System.Collections.Immutable;
using System.CommandLine;
Expand Down Expand Up @@ -65,7 +66,7 @@ public class ProjectManager : IDisposable {
/// </summary>
private int version;

private int openFileCount;
private ConcurrentDictionary<Uri, int> openFiles = new();

private VerifyOnMode AutomaticVerificationMode => options.Get(Verification);

Expand Down Expand Up @@ -234,8 +235,8 @@ public void Save(TextDocumentIdentifier documentId) {
/// Needs to be thread-safe
/// </summary>
/// <returns></returns>
public bool CloseDocument() {
if (Interlocked.Decrement(ref openFileCount) == 0) {
public bool CloseDocument(Uri uri) {
if (openFiles.TryRemove(uri, out _) && openFiles.IsEmpty) {
CloseAsync();
return true;
}
Expand Down Expand Up @@ -345,7 +346,7 @@ IntervalTree<Position, Position> GetTree(Uri uri) {
}

public void OpenDocument(Uri uri, bool triggerCompilation) {
Interlocked.Increment(ref openFileCount);
openFiles.TryAdd(uri, 1);

if (triggerCompilation) {
StartNewCompilation();
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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 _);
}
}
Expand Down Expand Up @@ -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);
Expand Down
1 change: 1 addition & 0 deletions docs/dev/news/4833.fix
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
Removed one cause of need for restarting the IDE.

0 comments on commit 23a083b

Please sign in to comment.