Always have project mode on

Source/DafnyLanguageServer.Test/GutterStatus/LinearVerificationGutterStatusTester.cs

@@ -25,7 +25,6 @@ protected override async Task SetUp(Action<DafnyOptions> modifyOptions) {
 
  void ModifyOptions(DafnyOptions options) {
  options.Set(ServerCommand.LineVerificationStatus, true);
- options.Set(ServerCommand.ProjectMode, true);
  modifyOptions?.Invoke(options);
  }
  await base.SetUp(ModifyOptions);

Source/DafnyLanguageServer.Test/Lookup/GoToDefinitionTest.cs

@@ -13,7 +13,6 @@ public class GoToDefinitionTest : ClientBasedLanguageServerTest {
 
  [Fact]
  public async Task ExplicitProjectToGoDefinitionWorks() {
- await SetUp(o => o.Set(ServerCommand.ProjectMode, true));
  var sourceA = @"
 const a := 3;
 ".TrimStart();

Source/DafnyLanguageServer.Test/Lookup/HoverTest.cs

@@ -17,7 +17,6 @@ public class HoverTest : ClientBasedLanguageServerTest {
  protected override async Task SetUp(Action<DafnyOptions> modifyOptions = null) {
  void ModifyOptions(DafnyOptions options) {
  options.ProverOptions.Add("SOLVER=noop");
- options.Set(ServerCommand.ProjectMode, true);
  modifyOptions?.Invoke(options);
  }
 

Source/DafnyLanguageServer.Test/Lookup/HoverVerificationTest.cs

@@ -21,13 +21,6 @@ namespace Microsoft.Dafny.LanguageServer.IntegrationTest.Lookup {
  [Collection("Sequential Collection")] // Let slow tests run sequentially
  public class HoverVerificationTest : ClientBasedLanguageServerTest {
 
- protected override Task SetUp(Action<DafnyOptions> modifyOptions) {
- return base.SetUp(o => {
- o.Set(ServerCommand.ProjectMode, true);
- modifyOptions?.Invoke(o);
- });
- }
-
  private const int MaxTestExecutionTimeMs = 30000;
 
  [Fact(Timeout = MaxTestExecutionTimeMs)]

Source/DafnyLanguageServer.Test/ProjectFiles/CompetingProjectFilesTest.cs

@@ -12,13 +12,6 @@ namespace Microsoft.Dafny.LanguageServer.IntegrationTest.ProjectFiles;
 
 public class CompetingProjectFilesTest : ClientBasedLanguageServerTest {
 
- protected override Task SetUp(Action<DafnyOptions> modifyOptions) {
- return base.SetUp(o => {
- o.Set(ServerCommand.ProjectMode, true);
- modifyOptions?.Invoke(o);
- });
- }
-
 
  /// <summary>
  /// A project should only publish diagnostics for uris which it owns,

Source/DafnyLanguageServer.Test/ProjectFiles/MultipleFilesProjectTest.cs

@@ -13,43 +13,6 @@
 namespace Microsoft.Dafny.LanguageServer.IntegrationTest.ProjectFiles;
 
 public class MultipleFilesProjectTest : ClientBasedLanguageServerTest {
- protected override Task SetUp(Action<DafnyOptions> modifyOptions) {
- return base.SetUp(o => {
- o.Set(ServerCommand.ProjectMode, true);
- modifyOptions?.Invoke(o);
- });
- }
-
- [Fact]
- public async Task NoProjectModeWithProjectFileAndMultipleFiles() {
- await SetUp(o => {
- o.Set(ServerCommand.ProjectMode, false);
- });
- var producerSource = @"
-method Foo(x: int) { 
- var y: char := 3.0;
-}
-".TrimStart();
-
- var consumerSource = @"
-include ""A.dfy""
-method Bar() {
- Foo(true); 
-}
-";
-
- var directory = Path.Combine(Path.GetTempPath(), Path.GetRandomFileName());
- Directory.CreateDirectory(directory);
- await File.WriteAllTextAsync(Path.Combine(directory, DafnyProject.FileName), "");
- // The names A and B are important, because A must be alphabetically before B to trigger a particular cache without cloning bug 
- await File.WriteAllTextAsync(Path.Combine(directory, "A.dfy"), producerSource);
- await CreateAndOpenTestDocument(consumerSource, Path.Combine(directory, "B.dfy"));
-
- var consumerDiagnostics = await diagnosticsReceiver.AwaitNextNotificationAsync(CancellationToken);
- Assert.Equal(2, consumerDiagnostics.Diagnostics.Count());
- Assert.Contains(consumerDiagnostics.Diagnostics, diagnostic => diagnostic.Message.Contains("bool"));
- await AssertNoDiagnosticsAreComing(CancellationToken);
- }
 
  [Fact]
  public async Task OnDiskProducerResolutionErrors() {

Source/DafnyLanguageServer.Test/ProjectFiles/ProjectFilesTest.cs

@@ -69,14 +69,32 @@ await SetUp(options => {
  options.Set(Function.FunctionSyntaxOption, "3");
  options.Set(CommonOptionBag.WarnShadowing, true);
  });
- var filePath = Path.Combine(Directory.GetCurrentDirectory(), "ProjectFiles/TestFiles/noWarnShadowing.dfy");
- var source = await File.ReadAllTextAsync(filePath);
- source += "\nghost function Bar(): int { 3 }";
+ var source = @"
+method Foo() {
+ var x := 3;
+ if (true) {
+ var x := 4;
+ }
+}
 
- var doc1 = await CreateAndOpenTestDocument(source, "orphaned");
- var diagnostics1 = await GetLastDiagnostics(doc1, CancellationToken);
+ghost function Bar(): int { 3 }".TrimStart();
+
+ var projectFileSource = @"
+includes = [""**/*.dfy""]
+
+[options]
+warn-shadowing = false
+function-syntax = 4";
+
+ var directory = Path.Combine(Path.GetTempPath(), Path.GetRandomFileName());
+ Directory.CreateDirectory(directory);
+
+ var noProjectFile = await CreateAndOpenTestDocument(source, "orphaned.dfy");
+ var diagnostics1 = await GetLastDiagnostics(noProjectFile, CancellationToken);
  Assert.Single(diagnostics1); // Stops after parsing
- await CreateAndOpenTestDocument(source, filePath);
+
+ await File.WriteAllTextAsync(Path.Combine(directory, DafnyProject.FileName), projectFileSource);
+ await CreateAndOpenTestDocument(source, Path.Combine(directory, "source.dfy"));
  await AssertNoDiagnosticsAreComing(CancellationToken);
  }
 

Source/DafnyLanguageServer.Test/Refactoring/RenameTest.cs

@@ -118,13 +118,6 @@ protected async Task<string> SetUpProjectFile() {
  return tempDir;
  }
 
- protected override Task SetUp(Action<DafnyOptions> modifyOptions) {
- return base.SetUp(o => {
- o.Set(ServerCommand.ProjectMode, true);
- modifyOptions?.Invoke(o);
- });
- }
-
  /// <summary>
  /// Assert that after requesting a rename to <paramref name="newName"/>
  /// at the markup position in <paramref name="source"/>

Source/DafnyLanguageServer.Test/Synchronization/VerificationOrderTest.cs

@@ -16,7 +16,6 @@ public class VerificationOrderTest : ClientBasedLanguageServerTest {
  public async Task VerificationPriorityBasedOnChangesWorksWithMultipleFiles() {
  await SetUp(options => {
  options.Set(BoogieOptionBag.Cores, 1U);
- options.Set(ServerCommand.ProjectMode, true);
  options.Set(ServerCommand.Verification, VerifyOnMode.ChangeProject);
  });
 

Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs

@@ -23,7 +23,6 @@ public async Task RunWithMultipleSimilarDocuments() {
 }".TrimStart();
  await SetUp(options => {
  options.Set(ServerCommand.Verification, VerifyOnMode.Never);
- options.Set(ServerCommand.ProjectMode, true);
  });
  var directory = Path.Combine(Path.GetTempPath(), Path.GetRandomFileName());
  await CreateAndOpenTestDocument("", Path.Combine(directory, DafnyProject.FileName));

Source/DafnyLanguageServer.Test/Various/CompilationStatusNotificationTest.cs

@@ -24,9 +24,6 @@ public async Task MultipleDocuments() {
 method Foo() returns (x: int) ensures x / 2 == 1; {
  return 2;
 }".TrimStart();
- await SetUp(options => {
- options.Set(ServerCommand.ProjectMode, true);
- });
  var directory = Path.Combine(Path.GetTempPath(), Path.GetRandomFileName());
  Directory.CreateDirectory(directory);
  await CreateAndOpenTestDocument("", Path.Combine(directory, DafnyProject.FileName));

Source/DafnyLanguageServer/ServerCommand.cs

@@ -16,7 +16,6 @@ static ServerCommand() {
  DafnyOptions.RegisterLegacyBinding(VerifySnapshots, (options, u) => options.VerifySnapshots = (int)u);
 
  DooFile.RegisterNoChecksNeeded(
- ProjectMode,
  Verification,
  GhostIndicators,
  LineVerificationStatus,
@@ -46,11 +45,6 @@ static ServerCommand() {
 Send notifications about the verification status of each line in the program.
 ".TrimStart());
 
- public static readonly Option<bool> ProjectMode = new("--project-mode", () => false,
- "New mode with working with project files. Will become the default") {
- IsHidden = true
- };
-
  public static readonly Option<uint> VerifySnapshots = new("--cache-verification", @"
 (experimental)
 0 - do not use any verification result caching (default)
@@ -64,7 +58,6 @@ related locations
  };
 
  public IEnumerable<Option> Options => new Option[] {
- ProjectMode,
  BoogieOptionBag.NoVerify,
  Verification,
  GhostIndicators,

Source/DafnyLanguageServer/Workspace/ProjectManagerDatabase.cs

@@ -198,12 +198,6 @@ public static DafnyProject ImplicitProject(Uri uri) {
  folder = Path.GetDirectoryName(folder);
  }
 
- if (projectFile != null && projectFile.Uri != sourceUri && !serverOptions.Get(ServerCommand.ProjectMode)) {
- logger.LogDebug("Project file at {} will be ignored because project mode is disabled", projectFile.Uri);
- projectFile.Uri = sourceUri;
- projectFile.Includes = new[] { sourceUri.LocalPath };
- }
-
  return projectFile;
  }