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

3 files changed, 76 insertions, 55 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();

         }

diff --git a/Source/DafnyExtension/MenuProxy.cs b/Source/DafnyExtension/MenuProxy.cs
index fc0c0d1d..59afc448 100644
--- a/Source/DafnyExtension/MenuProxy.cs
+++ b/Source/DafnyExtension/MenuProxy.cs
@@ -85,7 +85,7 @@ namespace DafnyLanguage
       return activeTextView != null

                     && DafnyLanguage.ResolverTagger.ResolverTaggers.TryGetValue(activeTextView.TextBuffer, out resolver)

                     && resolver.Program != null

-                    && resolver.VerificationErrors.Any(err => !string.IsNullOrEmpty(err.Model));

+                    && resolver.VerificationErrors.Any(err => !string.IsNullOrEmpty(err.ModelText));

     }

 

     public void ShowErrorModel(IWpfTextView activeTextView)

@@ -94,14 +94,14 @@ namespace DafnyLanguage
       var show = activeTextView != null

                  && DafnyLanguage.ResolverTagger.ResolverTaggers.TryGetValue(activeTextView.TextBuffer, out resolver)

                  && resolver.Program != null

-                 && resolver.VerificationErrors.Any(err => err.IsSelected && !string.IsNullOrEmpty(err.Model));

+                 && resolver.VerificationErrors.Any(err => err.IsSelected && !string.IsNullOrEmpty(err.ModelText));

       if (show)

       {

-        var selectedError = resolver.VerificationErrors.FirstOrDefault(err => err.IsSelected && !string.IsNullOrEmpty(err.Model));

+        var selectedError = resolver.VerificationErrors.FirstOrDefault(err => err.IsSelected && !string.IsNullOrEmpty(err.ModelText));

 

         if (selectedError != null)

         {

-          DafnyMenuPackage.ShowErrorModelInBVD(selectedError.Model, selectedError.SelectedStateId);

+          DafnyMenuPackage.ShowErrorModelInBVD(selectedError.ModelText, selectedError.SelectedStateId);

         }

       }

     }

diff --git a/Source/DafnyExtension/ResolverTagger.cs b/Source/DafnyExtension/ResolverTagger.cs
index b1187054..81346c77 100644
--- a/Source/DafnyExtension/ResolverTagger.cs
+++ b/Source/DafnyExtension/ResolverTagger.cs
@@ -96,11 +96,13 @@ namespace DafnyLanguage
     public readonly DafnyError Error;

     public readonly ITrackingSpan Span;

     public readonly int Id;

-    public DafnyErrorStateResolverTag(DafnyError error, ITrackingSpan span, int id)

+    public readonly string Description;

+    public DafnyErrorStateResolverTag(DafnyError error, ITrackingSpan span, int id, string description)

     {

       Error = error;

       Span = span;

       Id = id;

+      Description = description;

     }

   }

 

@@ -278,9 +280,12 @@ namespace DafnyLanguage
             for (int i = 0; i < err.StateSpans.Length; i++)

             {

               var span = err.StateSpans[i];

+              var name = err.Model.States.ToArray()[i].Name;

+              var descStart = name.LastIndexOf(": ") + 2;

+              var description = 1 < descStart ? name.Substring(descStart) : "";

               if (span != null)

               {

-                yield return new TagSpan<IDafnyResolverTag>(span.GetSpan(currentSnapshot), new DafnyErrorStateResolverTag(err, span, i));

+                yield return new TagSpan<IDafnyResolverTag>(span.GetSpan(currentSnapshot), new DafnyErrorStateResolverTag(err, span, i, description));

               }

             }

           }

@@ -471,46 +476,53 @@ namespace DafnyLanguage
     public readonly string Message;

     protected readonly ITextSnapshot Snapshot;

     public readonly ITrackingSpan Span;

-    public readonly string Model;

-    private ITrackingSpan[] _stateSpans;

-    public ITrackingSpan[] StateSpans

+    public readonly string ModelText;

+    public Microsoft.Boogie.Model _model;

+    public Microsoft.Boogie.Model Model

     {

       get

       {

-        if (!string.IsNullOrEmpty(Model))

+        if (_model == null && !string.IsNullOrEmpty(ModelText))

         {

-          if (_stateSpans != null) { return _stateSpans; }

-          var locRegex = new Regex(@"\((\d+),(\d+)\)");

-          using (var rd = new StringReader(Model))

+          using (var rd = new StringReader(ModelText))

           {

-            var model = Microsoft.Boogie.Model.ParseModels(rd, null).ToArray();

-            Contract.Assert(model.Length == 1);

-            _stateSpans = model[0].States.Select(

-              cs =>

-              {

-                var match = locRegex.Match(cs.Name);

-                if (!match.Success)

-                {

-                  return null;

-                }

-                else

-                {

-                  var line = Math.Max(0, int.Parse(match.Groups[1].Value) - 1);

-                  var column = Math.Max(0, int.Parse(match.Groups[2].Value) - 1);

-                  var sLine = Snapshot.GetLineFromLineNumber(line);

-                  Contract.Assert(column <= sLine.Length);

-                  var sLength = Math.Max(0, Math.Min(sLine.Length - column, 0));

-                  return Snapshot.CreateTrackingSpan(sLine.Start + column, sLength, SpanTrackingMode.EdgeExclusive, TrackingFidelityMode.Forward);

-                }

-              }

-            ).ToArray();

-            return _stateSpans;

+            var models = Microsoft.Boogie.Model.ParseModels(rd, null).ToArray();

+            Contract.Assert(models.Length == 1);

+            _model = models[0];

           }

         }

-        else

-        {

-          return null;

+        return _model;

+      }

+    }

+    private ITrackingSpan[] _stateSpans;

+    public ITrackingSpan[] StateSpans

+    {

+      get

+      {

+        if (_stateSpans == null && Model != null)

+        {          

+          var model = Model;

+          var locRegex = new Regex(@"\((\d+),(\d+)\)");

+          _stateSpans = model.States.Select(

+           cs =>

+           {

+             var match = locRegex.Match(cs.Name);

+             if (!match.Success)

+             {

+               return null;

+             }

+             else

+             {

+               var line = Math.Max(0, int.Parse(match.Groups[1].Value) - 1);

+               var column = Math.Max(0, int.Parse(match.Groups[2].Value) - 1);

+               var sLine = Snapshot.GetLineFromLineNumber(line);

+               Contract.Assert(column <= sLine.Length);

+               var sLength = Math.Max(0, Math.Min(sLine.Length - column, 0));

+               return Snapshot.CreateTrackingSpan(sLine.Start + column, sLength, SpanTrackingMode.EdgeExclusive, TrackingFidelityMode.Forward);

+             }

+           }).ToArray();

         }

+        return _stateSpans;

       }

     }

     public int SelectedStateId { get; set; }

@@ -561,7 +573,7 @@ namespace DafnyLanguage
       Contract.Assert(Column <= sLine.Length);

       var sLength = Math.Max(0, Math.Min(sLine.Length - Column, 5));

       Span = snapshot.CreateTrackingSpan(sLine.Start + Column, sLength, SpanTrackingMode.EdgeExclusive, TrackingFidelityMode.Forward);

-      Model = model;

+      ModelText = model;

       _errorSelection = _errorSelectionSingleton;

       SelectedStateId = -1;

     }