DafnyExtension: Made it display the compilation output in the VS output pane.

5 files changed, 44 insertions, 21 deletions

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 955453ad..e98062ce 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -49,12 +49,14 @@ namespace Microsoft.Dafny {
     }

 

     public int ErrorCount;

+    public TextWriter ErrorWriter = Console.Out;

+

     void Error(string msg, params object[] args) {

       Contract.Requires(msg != null);

       Contract.Requires(args != null);

 

       string s = string.Format("Compilation error: " + msg, args);

-      Console.WriteLine(s);

+      ErrorWriter.WriteLine(s);

       wr.WriteLine("/* {0} */", s);

       ErrorCount++;

     }

diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index ba4a9d2c..ff2cbc8c 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -240,13 +240,19 @@ namespace Microsoft.Dafny
 

     #region Compilation

 

-    public static void CompileDafnyProgram(Dafny.Program dafnyProgram, string dafnyProgramName)

+    public static void CompileDafnyProgram(Dafny.Program dafnyProgram, string dafnyProgramName, TextWriter outputWriter = null)

     {

       Contract.Requires(dafnyProgram != null);

 

+      if (outputWriter == null)

+      {

+        outputWriter = Console.Out;

+      }

+

       // Compile the Dafny program into a string that contains the C# program

       StringWriter sw = new StringWriter();

       Dafny.Compiler compiler = new Dafny.Compiler(sw);

+      compiler.ErrorWriter = outputWriter;

       var hasMain = compiler.HasMain(dafnyProgram);

       if (DafnyOptions.O.RunAfterCompile && !hasMain) {

         // do no more

@@ -265,11 +271,11 @@ namespace Microsoft.Dafny
           target.Write(csharpProgram);

           if (completeProgram)

           {

-            Console.WriteLine("Compiled program written to {0}", targetFilename);

+            outputWriter.WriteLine("Compiled program written to {0}", targetFilename);

           }

           else

           {

-            Console.WriteLine("File {0} contains the partially compiled program", targetFilename);

+            outputWriter.WriteLine("File {0} contains the partially compiled program", targetFilename);

           }

         }

       }

@@ -281,7 +287,7 @@ namespace Microsoft.Dafny
       }

       else if (!CodeDomProvider.IsDefinedLanguage("CSharp"))

       {

-        Console.WriteLine("Error: cannot compile, because there is no provider configured for input language CSharp");

+        outputWriter.WriteLine("Error: cannot compile, because there is no provider configured for input language CSharp");

       }

       else

       {

@@ -302,26 +308,26 @@ namespace Microsoft.Dafny
 

         var cr = provider.CompileAssemblyFromSource(cp, csharpProgram);

         if (DafnyOptions.O.RunAfterCompile && cr.Errors.Count == 0) {

-          Console.WriteLine("Program compiled successfully");

-          Console.WriteLine("Running...");

-          Console.WriteLine();

+          outputWriter.WriteLine("Program compiled successfully");

+          outputWriter.WriteLine("Running...");

+          outputWriter.WriteLine();

           var entry = cr.CompiledAssembly.EntryPoint;

           try {

             entry.Invoke(null, new object[] { new string[0] });

           } catch (System.Reflection.TargetInvocationException e) {

-            Console.WriteLine("Error: Execution resulted in exception: {0}", e.Message);

-            Console.WriteLine(e.InnerException.ToString());

+            outputWriter.WriteLine("Error: Execution resulted in exception: {0}", e.Message);

+            outputWriter.WriteLine(e.InnerException.ToString());

           } catch (Exception e) {

-            Console.WriteLine("Error: Execution resulted in exception: {0}", e.Message);

-            Console.WriteLine(e.ToString());

+            outputWriter.WriteLine("Error: Execution resulted in exception: {0}", e.Message);

+            outputWriter.WriteLine(e.ToString());

           }

         } else if (cr.Errors.Count == 0) {

-          Console.WriteLine("Compiled assembly into {0}", cr.PathToAssembly);

+          outputWriter.WriteLine("Compiled assembly into {0}", cr.PathToAssembly);

         } else {

-          Console.WriteLine("Errors compiling program into {0}", cr.PathToAssembly);

+          outputWriter.WriteLine("Errors compiling program into {0}", cr.PathToAssembly);

           foreach (var ce in cr.Errors) {

-            Console.WriteLine(ce.ToString());

-            Console.WriteLine();

+            outputWriter.WriteLine(ce.ToString());

+            outputWriter.WriteLine();

           }

         }

       }

diff --git a/Source/DafnyExtension/DafnyDriver.cs b/Source/DafnyExtension/DafnyDriver.cs
index 5a71164e..0f16242c 100644
--- a/Source/DafnyExtension/DafnyDriver.cs
+++ b/Source/DafnyExtension/DafnyDriver.cs
@@ -170,10 +170,10 @@ namespace DafnyLanguage
 

     #region Compilation

 

-    public static void Compile(Dafny.Program dafnyProgram)

+    public static void Compile(Dafny.Program dafnyProgram, TextWriter outputWriter)

     {

       Microsoft.Dafny.DafnyOptions.O.SpillTargetCode = true;

-      Microsoft.Dafny.DafnyDriver.CompileDafnyProgram(dafnyProgram, dafnyProgram.Name);

+      Microsoft.Dafny.DafnyDriver.CompileDafnyProgram(dafnyProgram, dafnyProgram.Name, outputWriter);

     }

 

     #endregion

diff --git a/Source/DafnyExtension/MenuProxy.cs b/Source/DafnyExtension/MenuProxy.cs
index 59afc448..a67ba602 100644
--- a/Source/DafnyExtension/MenuProxy.cs
+++ b/Source/DafnyExtension/MenuProxy.cs
@@ -1,5 +1,6 @@
-using System;

+using System;

 using System.Collections.Generic;

+using System.IO;

 using System.Linq;

 using System.Text;

 using System.Threading.Tasks;

@@ -75,7 +76,8 @@ namespace DafnyLanguage
           && DafnyLanguage.ResolverTagger.ResolverTaggers.TryGetValue(activeTextView.TextBuffer, out resolver)

           && resolver.Program != null)

       {

-        DafnyMenuPackage.ExecuteAsCompiling(() => { DafnyDriver.Compile(resolver.Program); });

+        var outputWriter = new StringWriter();

+        DafnyMenuPackage.ExecuteAsCompiling(() => { DafnyDriver.Compile(resolver.Program, outputWriter); }, outputWriter);

       }

     }

 

diff --git a/Source/DafnyMenu/DafnyMenuPackage.cs b/Source/DafnyMenu/DafnyMenuPackage.cs
index 2ceaa91d..114ddf10 100644
--- a/Source/DafnyMenu/DafnyMenuPackage.cs
+++ b/Source/DafnyMenu/DafnyMenuPackage.cs
@@ -3,6 +3,7 @@ using System.ComponentModel.Design;
 using System.Diagnostics;

 using System.Drawing;

 using System.Globalization;

+using System.IO;

 using System.Linq;

 using System.Runtime.InteropServices;

 using Microsoft.VisualStudio.ComponentModelHost;

@@ -281,14 +282,26 @@ namespace DafnyLanguage.DafnyMenu
       toggleBVDCommand.Text = (BVDDisabled ? "Enable" : "Disable") + " BVD";

     }

 

-    public void ExecuteAsCompiling(Action action)

+    public void ExecuteAsCompiling(Action action, TextWriter outputWriter)

     {

       IVsStatusbar statusBar = (IVsStatusbar)GetGlobalService(typeof(SVsStatusbar));

       uint cookie = 0;

       statusBar.Progress(ref cookie, 1, "Compiling...", 0, 0);

 

+      var gowp = (IVsOutputWindowPane)GetService(typeof(SVsGeneralOutputWindowPane));

+      if (gowp != null)

+      {

+        gowp.Clear();

+      }

+

       action();

 

+      if (gowp != null)

+      {

+        gowp.OutputStringThreadSafe(outputWriter.ToString());

+        gowp.Activate();

+      }

+

       statusBar.Progress(ref cookie, 0, "", 0, 0);

     }