Feat: Support for --bprint in language server.

Source/DafnyDriver/DafnyDriver.cs

@@ -607,16 +607,16 @@ private static string BoogieProgramSuffix(string printFile, string suffix) {
     }
 
     public static IEnumerable<Tuple<string, Bpl.Program>> Translate(ExecutionEngineOptions options, Program dafnyProgram) {
-      var nmodules = Translator.VerifiableModules(dafnyProgram).Count();
+      var modulesCount = Translator.VerifiableModules(dafnyProgram).Count();
 
 
       foreach (var prog in Translator.Translate(dafnyProgram, dafnyProgram.Reporter)) {
 
         if (options.PrintFile != null) {
 
-          var nm = nmodules > 1 ? Dafny.DafnyMain.BoogieProgramSuffix(options.PrintFile, prog.Item1) : options.PrintFile;
+          var fileName = modulesCount > 1 ? Dafny.DafnyMain.BoogieProgramSuffix(options.PrintFile, prog.Item1) : options.PrintFile;
 
-          ExecutionEngine.PrintBplFile(options, nm, prog.Item2, false, false, options.PrettyPrint);
+          ExecutionEngine.PrintBplFile(options, fileName, prog.Item2, false, false, options.PrettyPrint);
         }
 
         yield return prog;

Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs

@@ -52,10 +52,17 @@ public async Task<IReadOnlyList<IImplementationTask>> GetVerificationTasksAsync(
 
       cancellationToken.ThrowIfCancellationRequested();
 
+      if (engine.Options.PrintFile != null) {
+        var moduleCount = Translator.VerifiableModules(program).Count();
+        foreach (var (suffix, boogieProgram) in translated) {
+          var fileName = moduleCount > 1 ? DafnyMain.BoogieProgramSuffix(engine.Options.PrintFile, suffix) : engine.Options.PrintFile;
+          ExecutionEngine.PrintBplFile(engine.Options, fileName, boogieProgram, false, false, engine.Options.PrettyPrint);
+        }
+      }
+
       return translated.SelectMany(t => {
         var (_, boogieProgram) = t;
-        var results = engine.GetImplementationTasks(boogieProgram);
-        return results;
+        return engine.GetImplementationTasks(boogieProgram);
       }).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