From 0442fec7c535124fb60f412c9c499ee11eaea5ea Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Sun, 14 Jul 2013 17:53:26 -0700
Subject: DafnyExtension: Worked on integrating BVD.

---
 Source/DafnyExtension/ProgressMargin.cs |  61 ++++++++++--------
 Source/DafnyExtension/ResolverTagger.cs |  41 +++++++-----
 Source/DafnyMenu/BvdToolWindow.cs       |  59 ++++++++++++++++++
 Source/DafnyMenu/DafnyMenu.csproj       |  22 +++++--
 Source/DafnyMenu/DafnyMenu.vsct         |  10 +++
 Source/DafnyMenu/DafnyMenuPackage.cs    | 106 ++++++++++++++++++++++++--------
 Source/DafnyMenu/Guids.cs               |   6 ++
 Source/DafnyMenu/PkgCmdID.cs            |   3 +-
 Source/DafnyMenu/Resources.Designer.cs  |   2 +-
 Source/DafnyMenu/Resources/Images.png   | Bin 989 -> 0 bytes
 Source/DafnyMenu/Resources/Package.ico  | Bin 2998 -> 0 bytes
 Source/DafnyMenu/VSPackage.resx         |  14 -----
 12 files changed, 234 insertions(+), 90 deletions(-)
 create mode 100644 Source/DafnyMenu/BvdToolWindow.cs
 delete mode 100644 Source/DafnyMenu/Resources/Images.png
 delete mode 100644 Source/DafnyMenu/Resources/Package.ico

(limited to 'Source')

diff --git a/Source/DafnyExtension/ProgressMargin.cs b/Source/DafnyExtension/ProgressMargin.cs
index 6ee12d95..8f4a22a2 100644
--- a/Source/DafnyExtension/ProgressMargin.cs
+++ b/Source/DafnyExtension/ProgressMargin.cs
@@ -96,6 +96,7 @@ namespace DafnyLanguage
     ErrorListProvider _errorProvider;
     ITextBuffer _buffer;
     ITextDocument _document;
+    private bool m_disposed;
 
     readonly DispatcherTimer timer;
 
@@ -126,31 +127,34 @@ namespace DafnyLanguage
 
     private void Dispose(bool disposing)
     {
-      if (!m_disposed)
+      lock (this)
       {
-        if (disposing)
+        if (!m_disposed)
         {
-          if (lastRequestId != null)
-          {
-            Microsoft.Boogie.ExecutionEngine.CancelRequest(lastRequestId);
-          }
-          if (_document.FilePath != null)
+          if (disposing)
           {
-            ProgressTaggers.Remove(_document.FilePath);
-          }
-          _buffer.Changed -= buffer_Changed;
-          timer.Tick -= UponIdle;
-          _errorProvider.Dispose();
-          _errorProvider = null;
-          ClearCachedVerificationResults();
-          if (resolver != null)
-          {
-            resolver.Dispose();
-            resolver = null;
+            if (lastRequestId != null)
+            {
+              Microsoft.Boogie.ExecutionEngine.CancelRequest(lastRequestId);
+            }
+            if (_document.FilePath != null)
+            {
+              ProgressTaggers.Remove(_document.FilePath);
+            }
+            _buffer.Changed -= buffer_Changed;
+            timer.Tick -= UponIdle;
+            _errorProvider.Dispose();
+            _errorProvider = null;
+            ClearCachedVerificationResults();
+            if (resolver != null)
+            {
+              resolver.Dispose();
+              resolver = null;
+            }
           }
-        }
 
-        m_disposed = true;
+          m_disposed = true;
+        }
       }
     }
 
@@ -320,14 +324,17 @@ namespace DafnyLanguage
       {
         bool success = DafnyDriver.Verify(program, errorListHolder, GetHashCode().ToString(), requestId, errorInfo =>
         {
-          errorInfo.BoogieErrorCode = null;
-          if (errorInfo.RequestId != null && RequestIdToSnapshot.ContainsKey(errorInfo.RequestId))
+          if (!m_disposed)
           {
-            var s = RequestIdToSnapshot[errorInfo.RequestId];
-            errorListHolder.AddError(new DafnyError(errorInfo.Tok.line - 1, errorInfo.Tok.col - 1, ErrorCategory.VerificationError, errorInfo.FullMsg, s, errorInfo.Model.ToString()), errorInfo.ImplementationName, requestId);
-            foreach (var aux in errorInfo.Aux)
+            errorInfo.BoogieErrorCode = null;
+            if (errorInfo.RequestId != null && RequestIdToSnapshot.ContainsKey(errorInfo.RequestId))
             {
-              errorListHolder.AddError(new DafnyError(aux.Tok.line - 1, aux.Tok.col - 1, ErrorCategory.AuxInformation, aux.FullMsg, s), errorInfo.ImplementationName, requestId);
+              var s = RequestIdToSnapshot[errorInfo.RequestId];
+              errorListHolder.AddError(new DafnyError(errorInfo.Tok.line - 1, errorInfo.Tok.col - 1, ErrorCategory.VerificationError, errorInfo.FullMsg, s, errorInfo.Model.ToString()), errorInfo.ImplementationName, requestId);
+              foreach (var aux in errorInfo.Aux)
+              {
+                errorListHolder.AddError(new DafnyError(aux.Tok.line - 1, aux.Tok.col - 1, ErrorCategory.AuxInformation, aux.FullMsg, s), errorInfo.ImplementationName, requestId);
+              }
             }
           }
         });
@@ -357,7 +364,7 @@ namespace DafnyLanguage
     }
 
     public event EventHandler<SnapshotSpanEventArgs> TagsChanged;
-    private bool m_disposed;
+
     IEnumerable<ITagSpan<ProgressGlyphTag>> ITagger<ProgressGlyphTag>.GetTags(NormalizedSnapshotSpanCollection spans) {
       if (spans.Count == 0) yield break;
       var targetSnapshot = spans[0].Snapshot;
diff --git a/Source/DafnyExtension/ResolverTagger.cs b/Source/DafnyExtension/ResolverTagger.cs
index 4f5f70fb..aad7217c 100644
--- a/Source/DafnyExtension/ResolverTagger.cs
+++ b/Source/DafnyExtension/ResolverTagger.cs
@@ -89,6 +89,7 @@ namespace DafnyLanguage
     readonly ITextBuffer _buffer;
     readonly ITextDocument _document;
     ErrorListProvider _errorProvider;
+    private bool m_disposed;
 
     // The 'Snapshot' and 'Program' fields should be updated and read together, so they are protected by "this"
     public ITextSnapshot Snapshot;  // may be null
@@ -172,7 +173,7 @@ namespace DafnyLanguage
       }
     }
 
-    public static readonly IDictionary<string, Dafny.Program> Programs = new ConcurrentDictionary<string, Dafny.Program>();
+    public static readonly IDictionary<string, ResolverTagger> ResolverTaggers = new ConcurrentDictionary<string, ResolverTagger>();
 
     internal ResolverTagger(ITextBuffer buffer, IServiceProvider serviceProvider, ITextDocumentFactoryService textDocumentFactory)
     {
@@ -193,27 +194,34 @@ namespace DafnyLanguage
 
     private void Dispose(bool disposing)
     {
-      if (!m_disposed)
+      lock (this)
       {
-        if (disposing)
+        if (!m_disposed)
         {
-          if (_errorProvider != null)
+          if (disposing)
           {
-            try
+            if (_errorProvider != null)
             {
-              _errorProvider.Tasks.Clear();
+              try
+              {
+                _errorProvider.Tasks.Clear();
+              }
+              catch (InvalidOperationException)
+              {
+                // this may occur if the SVsServiceProvider somehow has been uninstalled before our Dispose method is called
+              }
+              _errorProvider.Dispose();
+              _errorProvider = null;
             }
-            catch (InvalidOperationException)
+            BufferIdleEventUtil.RemoveBufferIdleEventListener(_buffer, ResolveBuffer);
+            if (_document != null)
             {
-              // this may occur if the SVsServiceProvider somehow has been uninstalled before our Dispose method is called
+              ResolverTaggers.Remove(_document.FilePath);
             }
-            _errorProvider.Dispose();
-            _errorProvider = null;
           }
-          BufferIdleEventUtil.RemoveBufferIdleEventListener(_buffer, ResolveBuffer);
-        }
 
-        m_disposed = true;
+          m_disposed = true;
+        }
       }
     }
 
@@ -262,7 +270,6 @@ namespace DafnyLanguage
     }
 
     public event EventHandler<SnapshotSpanEventArgs> TagsChanged;
-    private bool m_disposed;
 
     /// <summary>
     /// Calls the Dafny parser/resolver/type checker on the contents of the buffer, updates the Error List accordingly.
@@ -295,11 +302,11 @@ namespace DafnyLanguage
 
       if (program != null && _document != null)
       {
-        Programs[_document.FilePath] = program;
+        ResolverTaggers[_document.FilePath] = this;
       }
       else if (_document != null)
       {
-        Programs.Remove(_document.FilePath);
+        ResolverTaggers.Remove(_document.FilePath);
       }
 
       _resolutionErrors = newErrors;
@@ -311,7 +318,7 @@ namespace DafnyLanguage
     {
       lock (this) 
       {
-        if (_errorProvider != null)
+        if (_errorProvider != null && !m_disposed)
         {
           _errorProvider.SuspendRefresh();  // reduce flickering
           _errorProvider.Tasks.Clear();
diff --git a/Source/DafnyMenu/BvdToolWindow.cs b/Source/DafnyMenu/BvdToolWindow.cs
new file mode 100644
index 00000000..0316d558
--- /dev/null
+++ b/Source/DafnyMenu/BvdToolWindow.cs
@@ -0,0 +1,59 @@
+using System;
+using System.Collections;
+using System.ComponentModel;
+using System.Drawing;
+using System.Data;
+using System.Windows;
+using System.Runtime.InteropServices;
+using Microsoft.VisualStudio.Shell.Interop;
+using Microsoft.VisualStudio.Shell;
+
+namespace DafnyLanguage.DafnyMenu
+{
+  /// <summary>
+  /// This class implements the tool window exposed by this package and hosts a user control.
+  ///
+  /// In Visual Studio tool windows are composed of a frame (implemented by the shell) and a pane, 
+  /// usually implemented by the package implementer.
+  ///
+  /// This class derives from the ToolWindowPane class provided from the MPF in order to use its 
+  /// implementation of the IVsUIElementPane interface.
+  /// </summary>
+  [Guid(GuidList.guidToolWindowPersistanceString)]
+  public class BvdToolWindow : ToolWindowPane
+  {
+    private static readonly Lazy<Microsoft.Boogie.ModelViewer.Main> bvdInstance = new Lazy<Microsoft.Boogie.ModelViewer.Main>(() => new Microsoft.Boogie.ModelViewer.Main(new string[] { }, true));
+    
+    /// <summary>
+    /// Standard constructor for the tool window.
+    /// </summary>
+    public BvdToolWindow() :
+      base(null)
+    {
+      // Set the window title reading it from the resources.
+      this.Caption = "Boogie Verification Debugger";
+      // Set the image that will appear on the tab of the window frame
+      // when docked with an other window
+      // The resource ID correspond to the one defined in the resx file
+      // while the Index is the offset in the bitmap strip. Each image in
+      // the strip being 16x16.
+      // this.BitmapResourceID = 301;
+      // this.BitmapIndex = 1;
+
+      // This is the user control hosted by the tool window; Note that, even if this class implements IDisposable,
+      // we are not calling Dispose on this object. This is because ToolWindowPane calls Dispose on 
+      // the object returned by the Content property.
+      // base.Content = new MyControl();
+    }
+
+    public override System.Windows.Forms.IWin32Window Window
+    {
+      get { return bvdInstance.Value; }
+    }
+
+    public static Microsoft.Boogie.ModelViewer.Main BVD
+    {
+      get { return bvdInstance.Value; }
+    }
+  }
+}
diff --git a/Source/DafnyMenu/DafnyMenu.csproj b/Source/DafnyMenu/DafnyMenu.csproj
index 6cd493c6..7fb6cfab 100644
--- a/Source/DafnyMenu/DafnyMenu.csproj
+++ b/Source/DafnyMenu/DafnyMenu.csproj
@@ -52,13 +52,23 @@
     <Reference Include="Microsoft.VisualStudio.Shell.11.0, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />
     <Reference Include="Microsoft.VisualStudio.Shell.Immutable.10.0, Version=10.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />
     <Reference Include="Microsoft.VisualStudio.Shell.Interop" />
+    <Reference Include="Microsoft.VisualStudio.Shell.Interop.11.0, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">
+      <EmbedInteropTypes>True</EmbedInteropTypes>
+    </Reference>
     <Reference Include="Microsoft.VisualStudio.Shell.Interop.8.0, Version=8.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a" />
     <Reference Include="Microsoft.VisualStudio.Shell.Interop.9.0" />
     <Reference Include="Microsoft.VisualStudio.Shell.Interop.10.0" />
     <Reference Include="Microsoft.VisualStudio.Text.Logic, Version=11.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />
+    <Reference Include="ModelViewer">
+      <HintPath>..\..\..\boogie\Binaries\ModelViewer.dll</HintPath>
+    </Reference>
+    <Reference Include="PresentationCore" />
+    <Reference Include="PresentationFramework" />
     <Reference Include="System" />
     <Reference Include="System.Core" />
     <Reference Include="System.Design" />
+    <Reference Include="System.Windows.Forms" />
+    <Reference Include="WindowsBase" />
   </ItemGroup>
   <ItemGroup>
     <COMReference Include="EnvDTE">
@@ -72,6 +82,7 @@
     </COMReference>
   </ItemGroup>
   <ItemGroup>
+    <Compile Include="BvdToolWindow.cs" />
     <Compile Include="Guids.cs" />
     <Compile Include="Resources.Designer.cs">
       <AutoGen>True</AutoGen>
@@ -92,6 +103,7 @@
     <EmbeddedResource Include="VSPackage.resx">
       <MergeWithCTO>true</MergeWithCTO>
       <ManifestResourceName>VSPackage</ManifestResourceName>
+      <SubType>Designer</SubType>
     </EmbeddedResource>
   </ItemGroup>
   <ItemGroup>
@@ -102,20 +114,18 @@
   <ItemGroup>
     <VSCTCompile Include="DafnyMenu.vsct">
       <ResourceName>Menus.ctmenu</ResourceName>
+      <SubType>Designer</SubType>
     </VSCTCompile>
   </ItemGroup>
-  <ItemGroup>
-    <None Include="Resources\Images.png" />
-  </ItemGroup>
-  <ItemGroup>
-    <Content Include="Resources\Package.ico" />
-  </ItemGroup>
   <ItemGroup>
     <ProjectReference Include="..\DafnyExtension\DafnyExtension.csproj">
       <Project>{6e9a5e14-0763-471c-a129-80a879d9e7ba}</Project>
       <Name>DafnyExtension</Name>
     </ProjectReference>
   </ItemGroup>
+  <ItemGroup>
+    <Folder Include="Resources\" />
+  </ItemGroup>
   <PropertyGroup>
     <UseCodebase>true</UseCodebase>
   </PropertyGroup>
diff --git a/Source/DafnyMenu/DafnyMenu.vsct b/Source/DafnyMenu/DafnyMenu.vsct
index 5cb2975d..25c8dea9 100644
--- a/Source/DafnyMenu/DafnyMenu.vsct
+++ b/Source/DafnyMenu/DafnyMenu.vsct
@@ -103,6 +103,15 @@
         </Strings>
       </Button>
 
+      <Button guid="guidDafnyMenuCmdSet" id="cmdidShowErrorModel" priority="0x010a" type="Button">
+        <Parent guid="guidDafnyMenuCmdSet" id="DafnyMenuGroup" />
+        <CommandFlag>DynamicVisibility</CommandFlag>
+        <CommandFlag>DefaultInvisible</CommandFlag>
+        <Strings>
+          <ButtonText>Show error model</ButtonText>
+        </Strings>
+      </Button>
+
     </Buttons>
 
     <!--The bitmaps section is used to define the bitmaps that are used for the commands.-->
@@ -133,6 +142,7 @@
       <IDSymbol name="cmdidRunVerifier" value="0x0101" />
       <IDSymbol name="cmdidStopVerifier" value="0x0102" />
       <IDSymbol name="cmdidToggleSnapshotVerification" value="0x0103" />
+      <IDSymbol name="cmdidShowErrorModel" value="0x0104" />
     </GuidSymbol>
 
     <!--
diff --git a/Source/DafnyMenu/DafnyMenuPackage.cs b/Source/DafnyMenu/DafnyMenuPackage.cs
index 294b0b75..1506e893 100644
--- a/Source/DafnyMenu/DafnyMenuPackage.cs
+++ b/Source/DafnyMenu/DafnyMenuPackage.cs
@@ -1,13 +1,12 @@
 using System;
+using System.ComponentModel.Design;
 using System.Diagnostics;
 using System.Globalization;
+using System.Linq;
 using System.Runtime.InteropServices;
-using System.ComponentModel.Design;
-using Microsoft.Win32;
-using Microsoft.VisualStudio;
-using Microsoft.VisualStudio.Shell.Interop;
-using Microsoft.VisualStudio.OLE.Interop;
 using Microsoft.VisualStudio.Shell;
+using Microsoft.VisualStudio.Shell.Interop;
+
 
 namespace DafnyLanguage.DafnyMenu
 {
@@ -26,10 +25,12 @@ namespace DafnyLanguage.DafnyMenu
   [PackageRegistration(UseManagedResourcesOnly = true)]
   // This attribute is used to register the information needed to show this package
   // in the Help/About dialog of Visual Studio.
-  [InstalledProductRegistration("#110", "#112", "1.0", IconResourceID = 400)]
+  [InstalledProductRegistration("#110", "#112", "1.0")]
   // This attribute is needed to let the shell know that this package exposes some menus.
   [ProvideMenuResource("Menus.ctmenu", 1)]
   [ProvideAutoLoad("{6c7ed99a-206a-4937-9e08-b389de175f68}")]
+  [ProvideToolWindow(typeof(BvdToolWindow), Transient = true)]
+  [ProvideToolWindowVisibility(typeof(BvdToolWindow), GuidList.guidDafnyMenuCmdSetString)]
   [Guid(GuidList.guidDafnyMenuPkgString)]
   public sealed class DafnyMenuPackage : Package
   {
@@ -39,6 +40,7 @@ namespace DafnyLanguage.DafnyMenu
     private OleMenuCommand runVerifierCommand;
     private OleMenuCommand stopVerifierCommand;
     private OleMenuCommand toggleSnapshotVerificationCommand;
+    private OleMenuCommand showErrorModelCommand;
 
     /// <summary>
     /// Default constructor of the package.
@@ -92,6 +94,12 @@ namespace DafnyLanguage.DafnyMenu
         toggleSnapshotVerificationCommand = new OleMenuCommand(ToggleSnapshotVerificationCallback, toggleSnapshotVerificationCommandID);
         mcs.AddCommand(toggleSnapshotVerificationCommand);
 
+        var showErrorModelCommandID = new CommandID(GuidList.guidDafnyMenuCmdSet, (int)PkgCmdIDList.cmdidShowErrorModel);
+        showErrorModelCommand = new OleMenuCommand(ShowErrorModelCallback, showErrorModelCommandID);
+        showErrorModelCommand.Enabled = true;
+        showErrorModelCommand.BeforeQueryStatus += showErrorModelCommand_BeforeQueryStatus;
+        mcs.AddCommand(showErrorModelCommand);
+
         var menuCommandID = new CommandID(GuidList.guidDafnyMenuPkgSet, (int)PkgCmdIDList.cmdidMenu);
         menuCommand = new OleMenuCommand(new EventHandler((sender, e) => { }), menuCommandID);
         menuCommand.BeforeQueryStatus += menuCommand_BeforeQueryStatus;
@@ -110,8 +118,7 @@ namespace DafnyLanguage.DafnyMenu
     {
       var dte = GetGlobalService(typeof(EnvDTE.DTE)) as EnvDTE.DTE;
       DafnyLanguage.ProgressTagger tagger;
-      DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(dte.ActiveDocument.FullName, out tagger);
-      if (tagger != null)
+      if (dte.ActiveDocument != null && DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(dte.ActiveDocument.FullName, out tagger))
       {
         tagger.StopVerification();
       }
@@ -121,8 +128,7 @@ namespace DafnyLanguage.DafnyMenu
     {
       var dte = GetGlobalService(typeof(EnvDTE.DTE)) as EnvDTE.DTE;
       DafnyLanguage.ProgressTagger tagger;
-      DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(dte.ActiveDocument.FullName, out tagger);
-      if (tagger != null)
+      if (dte.ActiveDocument != null && DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(dte.ActiveDocument.FullName, out tagger))
       {
         tagger.StartVerification();
       }
@@ -131,7 +137,8 @@ namespace DafnyLanguage.DafnyMenu
     void menuCommand_BeforeQueryStatus(object sender, EventArgs e)
     {
       var dte = GetGlobalService(typeof(EnvDTE.DTE)) as EnvDTE.DTE;
-      var isActive = dte.ActiveDocument.FullName.EndsWith(".dfy", StringComparison.OrdinalIgnoreCase);
+      var isActive = dte.ActiveDocument != null
+                     && dte.ActiveDocument.FullName.EndsWith(".dfy", StringComparison.OrdinalIgnoreCase);
       menuCommand.Visible = isActive;
       menuCommand.Enabled = isActive;
     }
@@ -140,26 +147,32 @@ namespace DafnyLanguage.DafnyMenu
     {
       var dte = GetGlobalService(typeof(EnvDTE.DTE)) as EnvDTE.DTE;
       DafnyLanguage.ProgressTagger tagger;
-      DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(dte.ActiveDocument.FullName, out tagger);
-      runVerifierCommand.Visible = tagger != null && tagger.VerificationDisabled;
-      runVerifierCommand.Enabled = tagger != null && tagger.VerificationDisabled;
+      var enabled = dte.ActiveDocument != null
+                 && DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(dte.ActiveDocument.FullName, out tagger)
+                 && tagger != null && tagger.VerificationDisabled;
+      runVerifierCommand.Visible = enabled;
+      runVerifierCommand.Enabled = enabled;
     }
 
     void stopVerifierCommand_BeforeQueryStatus(object sender, EventArgs e)
     {
       var dte = GetGlobalService(typeof(EnvDTE.DTE)) as EnvDTE.DTE;
       DafnyLanguage.ProgressTagger tagger;
-      DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(dte.ActiveDocument.FullName, out tagger);
-      stopVerifierCommand.Visible = !(tagger != null && tagger.VerificationDisabled);
-      stopVerifierCommand.Enabled = !(tagger != null && tagger.VerificationDisabled);
+      var disabled = dte.ActiveDocument != null
+                    && DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(dte.ActiveDocument.FullName, out tagger)
+                    && tagger != null && tagger.VerificationDisabled;
+      stopVerifierCommand.Visible = !disabled;
+      stopVerifierCommand.Enabled = !disabled;
     }
 
     void compileCommand_BeforeQueryStatus(object sender, EventArgs e)
     {
       var dte = GetGlobalService(typeof(EnvDTE.DTE)) as EnvDTE.DTE;
-      Microsoft.Dafny.Program program;
-      DafnyLanguage.ResolverTagger.Programs.TryGetValue(dte.ActiveDocument.FullName, out program);
-      compileCommand.Enabled = (program != null);
+      ResolverTagger resolver;
+      var enabled = dte.ActiveDocument != null
+                    && DafnyLanguage.ResolverTagger.ResolverTaggers.TryGetValue(dte.ActiveDocument.FullName, out resolver)
+                    && resolver.Program != null;
+      compileCommand.Enabled = enabled;
     }
 
     #endregion
@@ -173,19 +186,64 @@ namespace DafnyLanguage.DafnyMenu
     private void CompileCallback(object sender, EventArgs e)
     {
       var dte = GetGlobalService(typeof(EnvDTE.DTE)) as EnvDTE.DTE;
-      Microsoft.Dafny.Program program;
-      DafnyLanguage.ResolverTagger.Programs.TryGetValue(dte.ActiveDocument.FullName, out program);
+      ResolverTagger resolver;
 
-      if (program != null)
+      if (dte.ActiveDocument != null
+          && DafnyLanguage.ResolverTagger.ResolverTaggers.TryGetValue(dte.ActiveDocument.FullName, out resolver)
+          && resolver.Program != null)
       {
         IVsStatusbar statusBar = (IVsStatusbar)GetGlobalService(typeof(SVsStatusbar));
         uint cookie = 0;
         statusBar.Progress(ref cookie, 1, "Compiling...", 0, 0);
 
-        DafnyDriver.Compile(program);
+        DafnyDriver.Compile(resolver.Program);
 
         statusBar.Progress(ref cookie, 0, "", 0, 0);
       }
     }
+
+    /// <summary>
+    /// Show error model.
+    /// </summary>
+    /// <param name="sender"></param>
+    /// <param name="e"></param>
+    void showErrorModelCommand_BeforeQueryStatus(object sender, EventArgs e)
+    {
+      var dte = GetGlobalService(typeof(EnvDTE.DTE)) as EnvDTE.DTE;
+      ResolverTagger resolver;
+      var visible = dte.ActiveDocument != null
+                    && DafnyLanguage.ResolverTagger.ResolverTaggers.TryGetValue(dte.ActiveDocument.FullName, out resolver)
+                    && resolver.Program != null
+                    && resolver.VerificationErrors.Any(err => !string.IsNullOrEmpty(err.Model));
+      showErrorModelCommand.Visible = false; // TODO(wuestholz): Enable this.
+    }
+
+    private void ShowErrorModelCallback(object sender, EventArgs e)
+    {
+      var dte = GetGlobalService(typeof(EnvDTE.DTE)) as EnvDTE.DTE;
+      ResolverTagger resolver = null;
+      var show = dte.ActiveDocument != null
+                 && DafnyLanguage.ResolverTagger.ResolverTaggers.TryGetValue(dte.ActiveDocument.FullName, out resolver)
+                 && resolver.Program != null
+                 && resolver.VerificationErrors.Any(err => !string.IsNullOrEmpty(err.Model));
+      if (show)
+      {
+        var window = this.FindToolWindow(typeof(BvdToolWindow), 0, true);
+        if ((window == null) || (window.Frame == null))
+        {
+          throw new NotSupportedException("Can not create BvdToolWindow.");
+        }
+
+        var models = resolver.VerificationErrors.Select(err => err.Model).Where(m => !string.IsNullOrEmpty(m)).ToArray();
+
+        for (int i = 0; i < models.Length; i++)
+        {
+          BvdToolWindow.BVD.ReadModel(models[i], i);
+        }
+
+        IVsWindowFrame windowFrame = (IVsWindowFrame)window.Frame;
+        Microsoft.VisualStudio.ErrorHandler.ThrowOnFailure(windowFrame.Show());
+      }
+    }
   }
 }
diff --git a/Source/DafnyMenu/Guids.cs b/Source/DafnyMenu/Guids.cs
index dc392c09..8013d590 100644
--- a/Source/DafnyMenu/Guids.cs
+++ b/Source/DafnyMenu/Guids.cs
@@ -11,5 +11,11 @@ namespace DafnyLanguage.DafnyMenu
 
     public static readonly Guid guidDafnyMenuCmdSet = new Guid(guidDafnyMenuCmdSetString);
     public static readonly Guid guidDafnyMenuPkgSet = new Guid(guidDafnyMenuPkgString);
+
+    public const string guidBvdToolboxPkgString = "8b93ddf6-009c-46b9-a0d2-628405a4e466";
+    public const string guidBvdToolboxCmdSetString = "11635790-762b-495f-8c85-9de3a8fe91bd";
+    public const string guidToolWindowPersistanceString = "6f1cb50b-18fa-4d03-b480-71be56c50053";
+
+    public static readonly Guid guidBvdToolboxCmdSet = new Guid(guidBvdToolboxCmdSetString);
   };
 }
\ No newline at end of file
diff --git a/Source/DafnyMenu/PkgCmdID.cs b/Source/DafnyMenu/PkgCmdID.cs
index 0cf3869e..f5905ea3 100644
--- a/Source/DafnyMenu/PkgCmdID.cs
+++ b/Source/DafnyMenu/PkgCmdID.cs
@@ -10,6 +10,7 @@ namespace DafnyLanguage.DafnyMenu
     public const uint cmdidRunVerifier = 0x101;
     public const uint cmdidStopVerifier = 0x102;
     public const uint cmdidMenu = 0x1021;
-    public static int cmdidToggleSnapshotVerification = 0x103;
+    public static uint cmdidToggleSnapshotVerification = 0x103;
+    public const uint cmdidShowErrorModel = 0x104;
   };
 }
\ No newline at end of file
diff --git a/Source/DafnyMenu/Resources.Designer.cs b/Source/DafnyMenu/Resources.Designer.cs
index d934633f..c58dad40 100644
--- a/Source/DafnyMenu/Resources.Designer.cs
+++ b/Source/DafnyMenu/Resources.Designer.cs
@@ -1,7 +1,7 @@
 //------------------------------------------------------------------------------
 // <auto-generated>
 //     This code was generated by a tool.
-//     Runtime Version:4.0.30319.18033
+//     Runtime Version:4.0.30319.18051
 //
 //     Changes to this file may cause incorrect behavior and will be lost if
 //     the code is regenerated.
diff --git a/Source/DafnyMenu/Resources/Images.png b/Source/DafnyMenu/Resources/Images.png
deleted file mode 100644
index 51fe0d15..00000000
Binary files a/Source/DafnyMenu/Resources/Images.png and /dev/null differ
diff --git a/Source/DafnyMenu/Resources/Package.ico b/Source/DafnyMenu/Resources/Package.ico
deleted file mode 100644
index 449296f4..00000000
Binary files a/Source/DafnyMenu/Resources/Package.ico and /dev/null differ
diff --git a/Source/DafnyMenu/VSPackage.resx b/Source/DafnyMenu/VSPackage.resx
index 8ab9cc50..effe10d4 100644
--- a/Source/DafnyMenu/VSPackage.resx
+++ b/Source/DafnyMenu/VSPackage.resx
@@ -1,14 +1,4 @@
 <?xml version="1.0" encoding="utf-8"?>
-<!--
-    VS SDK Notes: This resx file contains the resources that will be consumed from your package by Visual Studio.
-    For example, Visual Studio will attempt to load resource '400' from this resource stream when it needs to
-    load your package's icon. Because Visual Studio will always look in the VSPackage.resources stream first for
-    resources it needs, you should put additional resources that Visual Studio will load directly into this resx 
-    file. 
-
-    Resources that you would like to access directly from your package in a strong-typed fashion should be stored 
-    in Resources.resx or another resx file.
--->
 <root>
   <!-- 
     Microsoft ResX Schema 
@@ -127,14 +117,10 @@
   <resheader name="writer">
     <value>System.Resources.ResXResourceWriter, System.Windows.Forms, Version=4.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089</value>
   </resheader>
-  <assembly alias="System.Windows.Forms" name="System.Windows.Forms, Version=4.0.0.0, Culture=neutral, PublicKeyToken=b77a5c561934e089" />
   <data name="110" xml:space="preserve">
     <value>DafnyMenu</value>
   </data>
   <data name="112" xml:space="preserve">
     <value>This is a menu for invoking Dafny.</value>
   </data>
-  <data name="400" type="System.Resources.ResXFileRef, System.Windows.Forms">
-    <value>Resources\Package.ico;System.Drawing.Icon, System.Drawing, Version=4.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a</value>
-  </data>
 </root>
\ No newline at end of file
-- 
cgit v1.2.3