Feat: Support for --bprint in language server.

I add this as a way to simplify boogie debugging, especially in cases when VSCode is not consistent with the command-line like in #4205

I did not add any test for that as it's meant for Dafny development only, but I tested it manually. I borrowed the code from the driver.

Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs

@@ -42,6 +42,7 @@ public async Task<IReadOnlyList<IImplementationTask>> GetVerificationTasksAsync(
  CancellationToken cancellationToken) {
  var program = document.Program;
  var errorReporter = (DiagnosticErrorReporter)program.Reporter;
+ var nmodules = Translator.VerifiableModules(program).Count();
 
  cancellationToken.ThrowIfCancellationRequested();
 
@@ -55,6 +56,12 @@ public async Task<IReadOnlyList<IImplementationTask>> GetVerificationTasksAsync(
  return translated.SelectMany(t => {
  var (_, boogieProgram) = t;
  var results = engine.GetImplementationTasks(boogieProgram);
+ if (engine.Options.PrintFile != null) {
+
+ var nm = nmodules > 1 ? DafnyMain.BoogieProgramSuffix(engine.Options.PrintFile, t.Item1) : engine.Options.PrintFile;
+
+ ExecutionEngine.PrintBplFile(engine.Options, nm, t.Item2, false, false, engine.Options.PrettyPrint);
+ }
  return results;
  }).ToList();
  }

Source/DafnyLanguageServer/ServerCommand.cs

@@ -59,6 +59,7 @@ related locations
  GhostIndicators,
  LineVerificationStatus,
  VerifySnapshots,
+ DeveloperOptionBag.BoogiePrint,
  CommonOptionBag.EnforceDeterminism,
  CommonOptionBag.UseJavadocLikeDocstringRewriterOption
  }.Concat(ICommandSpec.VerificationOptions).

docs/dev/news/bprint-option-in language-server.feat

@@ -0,0 +1 @@
+Support for the `--bprint` option for language server arguments