From 04026edf3d0e905362a51995f246d3c2c0807c81 Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Sat, 3 Aug 2013 18:05:42 -0700
Subject: DafnyExtension: Did some refactoring and added a description to error
 states.

---
 Source/DafnyExtension/ResolverTagger.cs | 82 +++++++++++++++++++--------------
 1 file changed, 47 insertions(+), 35 deletions(-)

(limited to 'Source/DafnyExtension/ResolverTagger.cs')

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;
     }
-- 
cgit v1.2.3