DafnyExtension: Made it select the last error state by default when an error is selected.

2 files changed, 14 insertions, 6 deletions

diff --git a/Source/DafnyExtension/ErrorModelTagger.cs b/Source/DafnyExtension/ErrorModelTagger.cs
index 781814b2..7cef93fb 100644
--- a/Source/DafnyExtension/ErrorModelTagger.cs
+++ b/Source/DafnyExtension/ErrorModelTagger.cs
@@ -164,6 +164,13 @@ namespace DafnyLanguage
       esrtag.Error.StateChangeEvent += new DafnyError.StateChangeEventHandler((o) =>

       {

         result.Visibility = esrtag.Error.IsSelected ? System.Windows.Visibility.Visible : System.Windows.Visibility.Collapsed;

+        var isSelected = esrtag.Error.IsSelected && esrtag.Error.SelectedStateId == esrtag.Id;

+        result.Stroke = isSelected ? Brushes.Black : Brushes.DodgerBlue;

+        result.ToolTip = isSelected ? "unselect state" : "select state";

+        if (isSelected)

+        {

+          esrtag.Error.SelectedStateAdornment = result;

+        }

       });

 

       result.MouseDown += new MouseButtonEventHandler((s, e) =>

@@ -240,10 +247,16 @@ namespace DafnyLanguage
 

           // select the new one

           ertag.Error.SelectedError = ertag.Error;

-          ertag.Error.SelectedError.Notify();

           ertag.Error.Adornment = result;

           ertag.Error.Adornment.Stroke = Brushes.Black;

           ertag.Error.Adornment.ToolTip = "unselect error";

+          if (!string.IsNullOrEmpty(ertag.Error.Model))

+          {

+            // select the last error state

+            ertag.Error.SelectedStateId = ertag.Error.StateSpans.Count() - 1;

+            DafnyClassifier.DafnyMenuPackage.ShowErrorModelInBVD(ertag.Error.Model, ertag.Error.SelectedStateId);

+          }

+          ertag.Error.SelectedError.Notify();

         }

       });

       return result;

diff --git a/Source/DafnyExtension/ResolverTagger.cs b/Source/DafnyExtension/ResolverTagger.cs
index dedf506a..230f79c5 100644
--- a/Source/DafnyExtension/ResolverTagger.cs
+++ b/Source/DafnyExtension/ResolverTagger.cs
@@ -376,11 +376,6 @@ namespace DafnyLanguage
               task.Navigate += new EventHandler(NavigateHandler);

             }

             _errorProvider.Tasks.Add(task);

-

-            if (err.Model != null)

-            {

-

-            }

           }

           _errorProvider.ResumeRefresh();

         }