DafnyExtension: Added support for selecting errors and showing the model in BVD.

2 files changed, 6 insertions, 7 deletions

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;