DafnyExtension: Did some refactoring and added a description to error states.

1 files changed, 25 insertions, 16 deletions

diff --git a/Source/DafnyExtension/ErrorModelTagger.cs b/Source/DafnyExtension/ErrorModelTagger.cs
index 76b0c10d..5fab67f3 100644
--- a/Source/DafnyExtension/ErrorModelTagger.cs
+++ b/Source/DafnyExtension/ErrorModelTagger.cs
@@ -86,7 +86,7 @@ namespace DafnyLanguage
       foreach (var tag in _aggregator.GetTags(spans))

       {

         var ertag = tag.Tag as DafnyErrorResolverTag;

-        if (ertag != null && ertag.Error.Model != null)

+        if (ertag != null && ertag.Error.ModelText != null)

         {

           NormalizedSnapshotSpanCollection normSpans = tag.Span.GetSpans(snapshot);

 

@@ -147,6 +147,11 @@ namespace DafnyLanguage
       }

     }

 

+    private static string ErrorStateToolTip(bool isSelected, string description)

+    {

+      return string.Format("{0}{1}", isSelected ? "unselect state" : "select state", !string.IsNullOrEmpty(description) ? " [" + description + "]" : "");

+    }

+

     private static Ellipse CreateErrorStateAdornment(DafnyErrorStateResolverTag esrtag)

     {

       var result = new Ellipse

@@ -154,7 +159,7 @@ namespace DafnyLanguage
         Fill = Brushes.DodgerBlue,

         Height = 12.0,

         Width = 12.0,

-        ToolTip = "select state",

+        ToolTip = ErrorStateToolTip(false, esrtag.Description),

         StrokeThickness = 3.0,

         Stroke = Brushes.DodgerBlue,

         Cursor = Cursors.Arrow,

@@ -166,9 +171,9 @@ namespace DafnyLanguage
         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)

         {

+          result.ToolTip = ErrorStateToolTip(isSelected, esrtag.Description);

           esrtag.Error.SelectedStateAdornment = result;

         }

       });

@@ -182,7 +187,7 @@ namespace DafnyLanguage
           esrtag.Error.SelectedStateAdornment = null;

           esrtag.Error.SelectedStateId = -1;

           result.Stroke = Brushes.DodgerBlue;

-          result.ToolTip = "select state";

+          result.ToolTip = result.ToolTip.ToString().Replace("unselect", "select");

         }

         else

         {

@@ -190,7 +195,7 @@ namespace DafnyLanguage
           if (esrtag.Error.SelectedStateAdornment != null)

           {

             esrtag.Error.SelectedStateAdornment.Stroke = Brushes.DodgerBlue;

-            esrtag.Error.SelectedStateAdornment.ToolTip = "select state";

+            esrtag.Error.SelectedStateAdornment.ToolTip = esrtag.Error.SelectedStateAdornment.ToolTip.ToString().Replace("unselect", "select");

             esrtag.Error.SelectedStateAdornment = null;

             esrtag.Error.SelectedStateId = -1;

           }

@@ -198,11 +203,11 @@ namespace DafnyLanguage
           // select the new one

           esrtag.Error.SelectedStateAdornment = result;

           esrtag.Error.SelectedStateAdornment.Stroke = Brushes.Black;

-          esrtag.Error.SelectedStateAdornment.ToolTip = "unselect state";

+          esrtag.Error.SelectedStateAdornment.ToolTip = ErrorStateToolTip(true, esrtag.Description);

           esrtag.Error.SelectedStateId = esrtag.Id;

-          if (!string.IsNullOrEmpty(esrtag.Error.Model))

+          if (!string.IsNullOrEmpty(esrtag.Error.ModelText))

           {

-            DafnyClassifier.DafnyMenuPackage.ShowErrorModelInBVD(esrtag.Error.Model, esrtag.Id);

+            DafnyClassifier.DafnyMenuPackage.ShowErrorModelInBVD(esrtag.Error.ModelText, esrtag.Id);

           }

         }

       });

@@ -221,18 +226,20 @@ namespace DafnyLanguage
         Stroke = Brushes.Crimson,

         Cursor = Cursors.Arrow,

       };

+

       result.Measure(new Size(double.PositiveInfinity, double.PositiveInfinity));

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

       {

         if (ertag.Error.IsSelected)

         {

           // unselect it

-          var selErr = ertag.Error.SelectedError;

-          ertag.Error.SelectedError = null;

-          ertag.Error.SelectedStateId = -1;

-          selErr.Notify();

+          var selErr = ertag.Error.SelectedError;          

+          selErr.SelectedStateId = -1;

+          selErr.SelectedStateAdornment = null;          

+          ertag.Error.SelectedError = null;          

           result.Stroke = Brushes.Crimson;

           result.ToolTip = "select error";

+          selErr.Notify();

         }

         else

         {

@@ -240,9 +247,10 @@ namespace DafnyLanguage
           if (ertag.Error.SelectedError != null)

           {

             var selErr = ertag.Error.SelectedError;

+            selErr.SelectedStateId = -1;

+            selErr.SelectedStateAdornment = null;

             selErr.Adornment.Stroke = Brushes.Crimson;

             selErr.Adornment.ToolTip = "select error";

-            ertag.Error.SelectedStateId = -1;

             ertag.Error.SelectedError = null;

             selErr.Notify();

           }

@@ -252,11 +260,12 @@ namespace DafnyLanguage
           ertag.Error.Adornment = result;

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

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

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

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

           {

             // select the last error state

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

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

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

+            ertag.Error.SelectedStateAdornment = null;

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

           }

           ertag.Error.SelectedError.Notify();

         }