From 832510796b7feb7f48cad8011aa688b2639668fa Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Mon, 15 Jul 2013 18:54:34 -0700
Subject: DafnyExtension: Added support for selecting errors and showing the
 model in BVD.

---
 Source/DafnyMenu/DafnyMenu.vsct      |  2 +-
 Source/DafnyMenu/DafnyMenuPackage.cs | 11 +++++------
 2 files changed, 6 insertions(+), 7 deletions(-)

(limited to 'Source/DafnyMenu')

diff --git a/Source/DafnyMenu/DafnyMenu.vsct b/Source/DafnyMenu/DafnyMenu.vsct
index 25c8dea9..d23ebc7f 100644
--- a/Source/DafnyMenu/DafnyMenu.vsct
+++ b/Source/DafnyMenu/DafnyMenu.vsct
@@ -108,7 +108,7 @@
         <CommandFlag>DynamicVisibility</CommandFlag>
         <CommandFlag>DefaultInvisible</CommandFlag>
         <Strings>
-          <ButtonText>Show error model</ButtonText>
+          <ButtonText>Show model for selected error in BVD</ButtonText>
         </Strings>
       </Button>
 
diff --git a/Source/DafnyMenu/DafnyMenuPackage.cs b/Source/DafnyMenu/DafnyMenuPackage.cs
index 1506e893..cb32f9fd 100644
--- a/Source/DafnyMenu/DafnyMenuPackage.cs
+++ b/Source/DafnyMenu/DafnyMenuPackage.cs
@@ -215,7 +215,7 @@ namespace DafnyLanguage.DafnyMenu
                     && 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.
+      showErrorModelCommand.Visible = visible;
     }
 
     private void ShowErrorModelCallback(object sender, EventArgs e)
@@ -225,7 +225,7 @@ namespace DafnyLanguage.DafnyMenu
       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));
+                 && resolver.VerificationErrors.Any(err => err.IsSelected && !string.IsNullOrEmpty(err.Model));
       if (show)
       {
         var window = this.FindToolWindow(typeof(BvdToolWindow), 0, true);
@@ -234,11 +234,10 @@ namespace DafnyLanguage.DafnyMenu
           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++)
+        var selectedError = resolver.VerificationErrors.FirstOrDefault(err => err.IsSelected && !string.IsNullOrEmpty(err.Model));
+        if (selectedError != null)
         {
-          BvdToolWindow.BVD.ReadModel(models[i], i);
+          BvdToolWindow.BVD.ReadModel(selectedError.Model);
         }
 
         IVsWindowFrame windowFrame = (IVsWindowFrame)window.Frame;
-- 
cgit v1.2.3