DafnyExtension: Worked on improving the error selection and visualization.

7 files changed, 233 insertions, 308 deletions

diff --git a/Source/DafnyExtension/DafnyExtension.csproj b/Source/DafnyExtension/DafnyExtension.csproj
index e5a679fd..a46feec3 100644
--- a/Source/DafnyExtension/DafnyExtension.csproj
+++ b/Source/DafnyExtension/DafnyExtension.csproj
@@ -191,7 +191,6 @@
     <Compile Include="GlobalSuppressions.cs" />

     <Compile Include="HoverText.cs" />

     <Compile Include="IdentifierTagger.cs" />

-    <Compile Include="IntraTextAdornmentTagger.cs" />

     <Compile Include="ProgressMargin.cs" />

     <Compile Include="OutliningTagger.cs" />

     <Compile Include="ResolverTagger.cs" />

diff --git a/Source/DafnyExtension/ErrorModelTagger.cs b/Source/DafnyExtension/ErrorModelTagger.cs
index 15e1c2ea..acb8ccb0 100644
--- a/Source/DafnyExtension/ErrorModelTagger.cs
+++ b/Source/DafnyExtension/ErrorModelTagger.cs
@@ -1,15 +1,8 @@
-//***************************************************************************

-// Copyright © 2010 Microsoft Corporation.  All Rights Reserved.

-// This code released under the terms of the

-// Microsoft Public License (MS-PL, http://opensource.org/licenses/ms-pl.html.)

-//***************************************************************************

-

-

-using System;

+using System;

 using System.Collections.Generic;

 using System.ComponentModel.Composition;

-using System.Diagnostics.Contracts;

 using System.Windows;

+using System.Windows.Controls;

 using System.Windows.Input;

 using System.Windows.Media;

 using System.Windows.Shapes;

@@ -27,7 +20,7 @@ namespace DafnyLanguage
   [Export(typeof(IViewTaggerProvider))]

   [ContentType("dafny")]

   [Name("ErrorModelTagger")]

-  [Order(After = "ErrorTagger")]

+  [Order(After = "ProgressTagger")]

   [TextViewRole(PredefinedTextViewRoles.Document)]

   [TagType(typeof(IntraTextAdornmentTag))]

   internal sealed class ErrorModelTaggerProvider : IViewTaggerProvider

@@ -59,7 +52,7 @@ namespace DafnyLanguage
 

   #region Tagger

 

-  internal sealed class ErrorModelTagger : IntraTextAdornmentTagger<IDafnyResolverTag, Ellipse>, IDisposable

+  internal sealed class ErrorModelTagger : ITagger<IntraTextAdornmentTag>, IDisposable

   {

     IWpfTextView _view;

     ITagAggregator<IDafnyResolverTag> _aggregator;

@@ -71,7 +64,6 @@ namespace DafnyLanguage
     }

 

     private ErrorModelTagger(IWpfTextView view, ITagAggregator<IDafnyResolverTag> aggregator)

-      : base(view)

     {

       _view = view;

       _aggregator = aggregator;

@@ -80,61 +72,150 @@ namespace DafnyLanguage
 

     public void Dispose()

     {

-      this._aggregator.Dispose();

-

-      base.view.Properties.RemoveProperty(typeof(ErrorModelTagger));

+      _aggregator.Dispose();

+      _view.Properties.RemoveProperty(typeof(ErrorModelTagger));

     }

 

-    // To produce adornments that don't obscure the text, the adornment tags

-    // should have zero length spans. Overriding this method allows control

-    // over the tag spans.

-    protected override IEnumerable<Tuple<SnapshotSpan, PositionAffinity?, IDafnyResolverTag>> GetAdornmentData(NormalizedSnapshotSpanCollection spans)

+    public IEnumerable<ITagSpan<IntraTextAdornmentTag>> GetTags(NormalizedSnapshotSpanCollection spans)

     {

-      if (spans.Count == 0)

-        yield break;

-

-      ITextSnapshot snapshot = spans[0].Snapshot;

+      if (spans.Count == 0) yield break;

+      var snapshot = spans[0].Snapshot;

 

-      var tags = this._aggregator.GetTags(spans);

-

-      foreach (IMappingTagSpan<IDafnyResolverTag> tag in tags)

+      var adornmentsPerSnapshot = new Dictionary<SnapshotSpan, List<Ellipse>>();

+      foreach (var tag in _aggregator.GetTags(spans))

       {

         var ertag = tag.Tag as DafnyErrorResolverTag;

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

         {

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

 

-          // Ignore data tags that are split by projection.

-          // This is theoretically possible but unlikely in current scenarios.

           if (normSpans.Count != 1)

             continue;

 

-          yield return Tuple.Create(new SnapshotSpan(normSpans[0].Start, 0), (PositionAffinity?)PositionAffinity.Successor, tag.Tag);

+          var adornment = _view.VisualElement.Dispatcher.Invoke(() => CreateErrorAdornment(ertag));

+          var span = new SnapshotSpan(normSpans[0].Start, 0);

+          List<Ellipse> adornments;

+          if (adornmentsPerSnapshot.TryGetValue(span, out adornments))

+          {

+            adornments.Add(adornment);

+          }

+          else

+          {

+            adornmentsPerSnapshot.Add(span, new List<Ellipse> { adornment });

+          }

+        }

+

+        var esrtag = tag.Tag as DafnyErrorStateResolverTag;

+        if (esrtag != null)

+        {

+          var adornment = _view.VisualElement.Dispatcher.Invoke(() => CreateErrorStateAdornment(esrtag));

+          var span = esrtag.Span.GetSpan(snapshot);

+          List<Ellipse> adornments;

+          if (adornmentsPerSnapshot.TryGetValue(span, out adornments))

+          {

+            adornments.Add(adornment);

+          }

+          else

+          {

+            adornmentsPerSnapshot.Add(span, new List<Ellipse> { adornment });

+          }

         }

       }

+

+      foreach (var adornments in adornmentsPerSnapshot)

+      {

+        var panel = _view.VisualElement.Dispatcher.Invoke(() =>

+          {

+            var p = new StackPanel

+            {

+              Orientation = Orientation.Horizontal,

+              Width = 12.0 * adornments.Value.Count,

+              Height = 12.0,

+            };

+            foreach (var adornment in adornments.Value)

+            {

+              p.Children.Add(adornment);

+            }

+            p.Measure(new Size(double.PositiveInfinity, double.PositiveInfinity));

+            return p;

+          });

+

+        yield return new TagSpan<IntraTextAdornmentTag>(adornments.Key, new IntraTextAdornmentTag(panel, null, PositionAffinity.Successor));

+      }

     }

 

-    protected override Ellipse CreateAdornment(IDafnyResolverTag data, SnapshotSpan span)

+    private static Ellipse CreateErrorStateAdornment(DafnyErrorStateResolverTag esrtag)

     {

-      var ertag = data as DafnyErrorResolverTag;

-      Contract.Assert(ertag != null);

-

       var result = new Ellipse

+      {

+        Fill = Brushes.Blue,

+        Height = 12.0,

+        Width = 12.0,

+        ToolTip = "select state",

+        StrokeThickness = 3.0,

+        Stroke = Brushes.Blue,

+        Cursor = Cursors.Arrow,

+        Visibility = System.Windows.Visibility.Collapsed

+      };

+

+      esrtag.Error.StateChangeEvent += new DafnyError.StateChangeEventHandler((o) =>

+      {

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

+      });

+

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

+      {

+        if (!esrtag.Error.IsSelected) { return; }

+        if (esrtag.Error.SelectedStateAdornment == result)

+        {

+          // unselect it

+          esrtag.Error.SelectedStateAdornment = null;

+          esrtag.Error.SelectedStateId = 0;

+          result.Stroke = Brushes.Blue;

+          result.ToolTip = "select state";

+        }

+        else

         {

-          Fill = Brushes.Red,

-          Height = 12.0, Width = 12.0,

-          ToolTip = "select error",

-          StrokeThickness = 3.0,

-          Stroke = Brushes.Red,

-          Cursor = Cursors.Arrow,

-          

-        };

+          // unselect the old one

+          if (esrtag.Error.SelectedStateAdornment != null)

+          {

+            esrtag.Error.SelectedStateAdornment.Stroke = Brushes.Blue;

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

+            esrtag.Error.SelectedStateAdornment = null;

+            esrtag.Error.SelectedStateId = 0;

+          }

+

+          // select the new one

+          esrtag.Error.SelectedStateAdornment = result;

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

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

+          esrtag.Error.SelectedStateId = esrtag.Id;

+        }

+      });

+      return result;

+    }

+

+    private static Ellipse CreateErrorAdornment(DafnyErrorResolverTag ertag)

+    {

+      var result = new Ellipse

+      {

+        Fill = Brushes.Red,

+        Height = 12.0,

+        Width = 12.0,

+        ToolTip = "select error",

+        StrokeThickness = 3.0,

+        Stroke = Brushes.Red,

+        Cursor = Cursors.Arrow,

+      };

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

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

       {

-        if (ertag.Error.SelectedError == ertag.Error)

+        if (ertag.Error.IsSelected)

         {

           // unselect it

+          var selErr = ertag.Error.SelectedError;

           ertag.Error.SelectedError = null;

+          selErr.Notify();

           result.Stroke = Brushes.Red;

           result.ToolTip = "select error";

         }

@@ -143,14 +224,17 @@ namespace DafnyLanguage
           // unselect the old one

           if (ertag.Error.SelectedError != null)

           {

-            ertag.Error.SelectedError.Adornment.Stroke = Brushes.Red;

-            ertag.Error.SelectedError.Adornment.ToolTip = "select error";

+            var selErr = ertag.Error.SelectedError;

+            selErr.Adornment.Stroke = Brushes.Red;

+            selErr.Adornment.ToolTip = "select error";

             ertag.Error.SelectedError = null;

+            selErr.Notify();

           }

 

           // select the new one

           ertag.Error.SelectedError = ertag.Error;

-          ertag.Error.Adornment = result;          

+          ertag.Error.SelectedError.Notify();

+          ertag.Error.Adornment = result;

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

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

         }

@@ -158,18 +242,19 @@ namespace DafnyLanguage
       return result;

     }

 

-    protected override bool UpdateAdornment(Ellipse adornment, IDafnyResolverTag data)

-    {

-      return false;

-    }

+    public event EventHandler<SnapshotSpanEventArgs> TagsChanged;

 

     void _aggregator_TagsChanged(object sender, TagsChangedEventArgs e)

-    {      

-      NormalizedSnapshotSpanCollection spans = e.Span.GetSpans(_view.TextBuffer.CurrentSnapshot);

-      if (spans.Count > 0)

+    {

+      var chng = TagsChanged;

+      if (chng != null)

       {

-        var span = new SnapshotSpan(spans[0].Start, spans[spans.Count - 1].End);

-        InvalidateSpans(new List<SnapshotSpan> { span });

+        NormalizedSnapshotSpanCollection spans = e.Span.GetSpans(_view.TextBuffer.CurrentSnapshot);

+        if (spans.Count > 0)

+        {

+          SnapshotSpan span = new SnapshotSpan(spans[0].Start, spans[spans.Count - 1].End);

+          chng(this, new SnapshotSpanEventArgs(span));

+        }

       }

     }

   }

diff --git a/Source/DafnyExtension/ErrorTagger.cs b/Source/DafnyExtension/ErrorTagger.cs
index 2b8a4708..9ac9ea07 100644
--- a/Source/DafnyExtension/ErrorTagger.cs
+++ b/Source/DafnyExtension/ErrorTagger.cs
@@ -60,7 +60,7 @@ namespace DafnyLanguage
     public IEnumerable<ITagSpan<IErrorTag>> GetTags(NormalizedSnapshotSpanCollection spans) {

       if (spans.Count == 0) yield break;

       var snapshot = spans[0].Snapshot;

-      foreach (var tagSpan in this._aggregator.GetTags(spans)) {

+      foreach (var tagSpan in _aggregator.GetTags(spans)) {

         var et = tagSpan.Tag as IErrorTag;

         if (et != null) {

           foreach (SnapshotSpan s in tagSpan.Span.GetSpans(snapshot)) {

diff --git a/Source/DafnyExtension/IntraTextAdornmentTagger.cs b/Source/DafnyExtension/IntraTextAdornmentTagger.cs
deleted file mode 100644
index 8d789d2f..00000000
--- a/Source/DafnyExtension/IntraTextAdornmentTagger.cs
+++ /dev/null
@@ -1,252 +0,0 @@
-//***************************************************************************

-//

-//    Copyright (c) Microsoft Corporation. All rights reserved.

-//    This code is licensed under the Visual Studio SDK license terms.

-//    THIS CODE IS PROVIDED *AS IS* WITHOUT WARRANTY OF

-//    ANY KIND, EITHER EXPRESS OR IMPLIED, INCLUDING ANY

-//    IMPLIED WARRANTIES OF FITNESS FOR A PARTICULAR

-//    PURPOSE, MERCHANTABILITY, OR NON-INFRINGEMENT.

-//

-//***************************************************************************

-

-using System;

-using System.Collections.Generic;

-using System.Linq;

-using System.Windows;

-using Microsoft.VisualStudio.Text;

-using Microsoft.VisualStudio.Text.Editor;

-using Microsoft.VisualStudio.Text.Tagging;

-

-namespace DafnyLanguage

-{

-  /// <summary>

-  /// Helper class for interspersing adornments into text.

-  /// </summary>

-  /// <remarks>

-  /// To avoid an issue around intra-text adornment support and its interaction with text buffer changes,

-  /// this tagger reacts to text and color tag changes with a delay. It waits to send out its own TagsChanged

-  /// event until the WPF Dispatcher is running again and it takes care to report adornments

-  /// that are consistent with the latest sent TagsChanged event by storing that particular snapshot

-  /// and using it to query for the data tags.

-  /// </remarks>

-  internal abstract class IntraTextAdornmentTagger<TData, TAdornment>

-      : ITagger<IntraTextAdornmentTag>

-      where TAdornment : UIElement

-  {

-    protected readonly IWpfTextView view;

-    private Dictionary<SnapshotSpan, TAdornment> adornmentCache = new Dictionary<SnapshotSpan, TAdornment>();

-    protected ITextSnapshot snapshot { get; private set; }

-    private readonly List<SnapshotSpan> invalidatedSpans = new List<SnapshotSpan>();

-

-    protected IntraTextAdornmentTagger(IWpfTextView view)

-    {

-      this.view = view;

-      this.snapshot = view.TextBuffer.CurrentSnapshot;

-

-      this.view.LayoutChanged += HandleLayoutChanged;

-      this.view.TextBuffer.Changed += HandleBufferChanged;

-    }

-

-    /// <param name="span">The span of text that this adornment will elide.</param>

-    /// <returns>Adornment corresponding to given data. May be null.</returns>

-    protected abstract TAdornment CreateAdornment(TData data, SnapshotSpan span);

-

-    /// <returns>True if the adornment was updated and should be kept. False to have the adornment removed from the view.</returns>

-    protected abstract bool UpdateAdornment(TAdornment adornment, TData data);

-

-    /// <param name="spans">Spans to provide adornment data for. These spans do not necessarily correspond to text lines.</param>

-    /// <remarks>

-    /// If adornments need to be updated, call <see cref="RaiseTagsChanged"/> or <see cref="InavlidateSpans"/>.

-    /// This will, indirectly, cause <see cref="GetAdornmentData"/> to be called.

-    /// </remarks>

-    /// <returns>

-    /// A sequence of:

-    ///  * adornment data for each adornment to be displayed

-    ///  * the span of text that should be elided for that adornment (zero length spans are acceptable)

-    ///  * and affinity of the adornment (this should be null if and only if the elided span has a length greater than zero)

-    /// </returns>

-    protected abstract IEnumerable<Tuple<SnapshotSpan, PositionAffinity?, TData>> GetAdornmentData(NormalizedSnapshotSpanCollection spans);

-

-    private void HandleBufferChanged(object sender, TextContentChangedEventArgs args)

-    {

-      var editedSpans = args.Changes.Select(change => new SnapshotSpan(args.After, change.NewSpan)).ToList();

-      InvalidateSpans(editedSpans);

-    }

-

-    /// <summary>

-    /// Causes intra-text adornments to be updated asynchronously.

-    /// </summary>

-    protected void InvalidateSpans(IList<SnapshotSpan> spans)

-    {

-      lock (this.invalidatedSpans)

-      {

-        bool wasEmpty = this.invalidatedSpans.Count == 0;

-        this.invalidatedSpans.AddRange(spans);

-

-        if (wasEmpty && this.invalidatedSpans.Count > 0)

-          this.view.VisualElement.Dispatcher.BeginInvoke(new Action(AsyncUpdate));

-      }

-    }

-

-    private void AsyncUpdate()

-    {

-      // Store the snapshot that we're now current with and send an event

-      // for the text that has changed.

-      if (this.snapshot != this.view.TextBuffer.CurrentSnapshot)

-      {

-        this.snapshot = this.view.TextBuffer.CurrentSnapshot;

-

-        Dictionary<SnapshotSpan, TAdornment> translatedAdornmentCache = new Dictionary<SnapshotSpan, TAdornment>();

-

-        foreach (var keyValuePair in this.adornmentCache)

-          translatedAdornmentCache.Add(keyValuePair.Key.TranslateTo(this.snapshot, SpanTrackingMode.EdgeExclusive), keyValuePair.Value);

-

-        this.adornmentCache = translatedAdornmentCache;

-      }

-

-      List<SnapshotSpan> translatedSpans;

-      lock (this.invalidatedSpans)

-      {

-        translatedSpans = this.invalidatedSpans.Select(s => s.TranslateTo(this.snapshot, SpanTrackingMode.EdgeInclusive)).ToList();

-        this.invalidatedSpans.Clear();

-      }

-

-      if (translatedSpans.Count == 0)

-        return;

-

-      var start = translatedSpans.Select(span => span.Start).Min();

-      var end = translatedSpans.Select(span => span.End).Max();

-

-      RaiseTagsChanged(new SnapshotSpan(start, end));

-    }

-

-    /// <summary>

-    /// Causes intra-text adornments to be updated synchronously.

-    /// </summary>

-    protected void RaiseTagsChanged(SnapshotSpan span)

-    {

-      var handler = this.TagsChanged;

-      if (handler != null)

-        handler(this, new SnapshotSpanEventArgs(span));

-    }

-

-    private void HandleLayoutChanged(object sender, TextViewLayoutChangedEventArgs e)

-    {

-      SnapshotSpan visibleSpan = this.view.TextViewLines.FormattedSpan;

-

-      // Filter out the adornments that are no longer visible.

-      List<SnapshotSpan> toRemove = new List<SnapshotSpan>(

-          from keyValuePair

-          in this.adornmentCache

-          where !keyValuePair.Key.TranslateTo(visibleSpan.Snapshot, SpanTrackingMode.EdgeExclusive).IntersectsWith(visibleSpan)

-          select keyValuePair.Key);

-

-      foreach (var span in toRemove)

-        this.adornmentCache.Remove(span);

-    }

-

-

-    // Produces tags on the snapshot that the tag consumer asked for.

-    public virtual IEnumerable<ITagSpan<IntraTextAdornmentTag>> GetTags(NormalizedSnapshotSpanCollection spans)

-    {

-      if (spans == null || spans.Count == 0)

-        yield break;

-

-      // Translate the request to the snapshot that this tagger is current with.

-

-      ITextSnapshot requestedSnapshot = spans[0].Snapshot;

-

-      var translatedSpans = new NormalizedSnapshotSpanCollection(spans.Select(span => span.TranslateTo(this.snapshot, SpanTrackingMode.EdgeExclusive)));

-

-      // Grab the adornments.

-      foreach (var tagSpan in GetAdornmentTagsOnSnapshot(translatedSpans))

-      {

-        // Translate each adornment to the snapshot that the tagger was asked about.

-        SnapshotSpan span = tagSpan.Span.TranslateTo(requestedSnapshot, SpanTrackingMode.EdgeExclusive);

-

-        IntraTextAdornmentTag tag = new IntraTextAdornmentTag(tagSpan.Tag.Adornment, tagSpan.Tag.RemovalCallback, tagSpan.Tag.Affinity);

-        yield return new TagSpan<IntraTextAdornmentTag>(span, tag);

-      }

-    }

-

-    // Produces tags on the snapshot that this tagger is current with.

-    private IEnumerable<TagSpan<IntraTextAdornmentTag>> GetAdornmentTagsOnSnapshot(NormalizedSnapshotSpanCollection spans)

-    {

-      if (spans.Count == 0)

-        yield break;

-

-      ITextSnapshot snapshot = spans[0].Snapshot;

-

-      System.Diagnostics.Debug.Assert(snapshot == this.snapshot);

-

-      // Since WPF UI objects have state (like mouse hover or animation) and are relatively expensive to create and lay out,

-      // this code tries to reuse controls as much as possible.

-      // The controls are stored in this.adornmentCache between the calls.

-

-      // Mark which adornments fall inside the requested spans with Keep=false

-      // so that they can be removed from the cache if they no longer correspond to data tags.

-      HashSet<SnapshotSpan> toRemove = new HashSet<SnapshotSpan>();

-      foreach (var ar in this.adornmentCache)

-        if (spans.IntersectsWith(new NormalizedSnapshotSpanCollection(ar.Key)))

-          toRemove.Add(ar.Key);

-

-      foreach (var spanDataPair in GetAdornmentData(spans).Distinct(new Comparer()))

-      {

-        // Look up the corresponding adornment or create one if it's new.

-        TAdornment adornment;

-        SnapshotSpan snapshotSpan = spanDataPair.Item1;

-        PositionAffinity? affinity = spanDataPair.Item2;

-        TData adornmentData = spanDataPair.Item3;

-        if (this.adornmentCache.TryGetValue(snapshotSpan, out adornment))

-        {

-          if (UpdateAdornment(adornment, adornmentData))

-            toRemove.Remove(snapshotSpan);

-        }

-        else

-        {

-          adornment = CreateAdornment(adornmentData, snapshotSpan);

-

-          if (adornment == null)

-            continue;

-

-          // Get the adornment to measure itself. Its DesiredSize property is used to determine

-          // how much space to leave between text for this adornment.

-          // Note: If the size of the adornment changes, the line will be reformatted to accommodate it.

-          // Note: Some adornments may change size when added to the view's visual tree due to inherited

-          // dependency properties that affect layout. Such options can include SnapsToDevicePixels,

-          // UseLayoutRounding, TextRenderingMode, TextHintingMode, and TextFormattingMode. Making sure

-          // that these properties on the adornment match the view's values before calling Measure here

-          // can help avoid the size change and the resulting unnecessary re-format.

-          adornment.Measure(new Size(double.PositiveInfinity, double.PositiveInfinity));

-

-          this.adornmentCache.Add(snapshotSpan, adornment);

-        }

-

-        yield return new TagSpan<IntraTextAdornmentTag>(snapshotSpan, new IntraTextAdornmentTag(adornment, null, affinity));

-      }

-

-      foreach (var snapshotSpan in toRemove)

-        this.adornmentCache.Remove(snapshotSpan);

-    }

-

-    public event EventHandler<SnapshotSpanEventArgs> TagsChanged;

-

-    private class Comparer : IEqualityComparer<Tuple<SnapshotSpan, PositionAffinity?, TData>>

-    {

-      public bool Equals(Tuple<SnapshotSpan, PositionAffinity?, TData> x, Tuple<SnapshotSpan, PositionAffinity?, TData> y)

-      {

-        if (x == null && y == null)

-          return true;

-        if (x == null || y == null)

-          return false;

-        return x.Item1.Equals(y.Item1);

-      }

-

-      public int GetHashCode(Tuple<SnapshotSpan, PositionAffinity?, TData> obj)

-      {

-        return obj.Item1.GetHashCode();

-      }

-    }

-

-  }

-}

diff --git a/Source/DafnyExtension/ProgressMargin.cs b/Source/DafnyExtension/ProgressMargin.cs
index a96a0373..9d10cb70 100644
--- a/Source/DafnyExtension/ProgressMargin.cs
+++ b/Source/DafnyExtension/ProgressMargin.cs
@@ -68,6 +68,7 @@ namespace DafnyLanguage
 

   [Export(typeof(ITaggerProvider))]

   [ContentType("dafny")]

+  [Name("ProgressTagger")]

   [TagType(typeof(ProgressGlyphTag))]

   class ProgressTaggerProvider : ITaggerProvider

   {

diff --git a/Source/DafnyExtension/ResolverTagger.cs b/Source/DafnyExtension/ResolverTagger.cs
index 7f1a7b4b..e9a62e4c 100644
--- a/Source/DafnyExtension/ResolverTagger.cs
+++ b/Source/DafnyExtension/ResolverTagger.cs
@@ -10,7 +10,9 @@ using System.Collections.Concurrent;
 using System.Collections.Generic;

 using System.ComponentModel.Composition;

 using System.Diagnostics.Contracts;

+using System.IO;

 using System.Linq;

+using System.Text.RegularExpressions;

 using System.Windows.Shapes;

 using Microsoft.VisualStudio;

 using Microsoft.VisualStudio.Shell;

@@ -89,6 +91,19 @@ namespace DafnyLanguage
     }

   }

 

+  public class DafnyErrorStateResolverTag : IDafnyResolverTag

+  {

+    public readonly DafnyError Error;

+    public readonly ITrackingSpan Span;

+    public readonly int Id;

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

+    {

+      Error = error;

+      Span = span;

+      Id = id;

+    }

+  }

+

   public class DafnySuccessResolverTag : IDafnyResolverTag

   {

     public readonly Dafny.Program Program;

@@ -257,6 +272,18 @@ namespace DafnyLanguage
         if (err.Category != ErrorCategory.ProcessError)

         {

           yield return new TagSpan<IDafnyResolverTag>(err.Span.GetSpan(currentSnapshot), new DafnyErrorResolverTag(err));

+

+          if (err.StateSpans != null)

+          {

+            for (int i = 0; i < err.StateSpans.Length; i++)

+            {

+              var span = err.StateSpans[i];

+              if (span != null)

+              {

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

+              }

+            }

+          }

         }

       }

 

@@ -447,12 +474,75 @@ namespace DafnyLanguage
     public readonly int Column;  // 0 based

     public readonly ErrorCategory Category;

     public readonly string Message;

+    protected readonly ITextSnapshot Snapshot;

     public readonly ITrackingSpan Span;

     public readonly string Model;

+    private ITrackingSpan[] _stateSpans;

+    public ITrackingSpan[] StateSpans

+    {

+      get

+      {

+        if (Model != null)

+        {

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

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

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

+          {

+            var model = Microsoft.Boogie.Model.ParseModels(rd).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;

+          }

+        }

+        else

+        {

+          return null;

+        }

+      }

+    }

+    public int SelectedStateId { get; set; }

+    public Shape SelectedStateAdornment { get; set; }

     public bool IsSelected { get { return SelectedError == this; } }

     private readonly ErrorSelection _errorSelection;

     public DafnyError SelectedError { get { return _errorSelection.Error; } set { _errorSelection.Error = value; } }

     public Shape Adornment;

+    public delegate void StateChangeEventHandler(object sender);

+    public event StateChangeEventHandler StateChangeEvent;

+    public void Notify()

+    {

+      if (StateChangeEvent != null)

+      {

+        StateChangeEvent(this);

+      }

+    }

+    public void UnsubscribeAll()

+    {

+      if (StateChangeEvent != null)

+      {

+        foreach (var d in StateChangeEvent.GetInvocationList())

+        {

+          StateChangeEvent -= (StateChangeEventHandler)d;

+        }

+      }

+    }

 

     internal class ErrorSelection

     {

@@ -471,6 +561,7 @@ namespace DafnyLanguage
       Column = Math.Max(0, col);

       Category = cat;

       Message = msg;

+      Snapshot = snapshot;

       var sLine = snapshot.GetLineFromLineNumber(line);

       Contract.Assert(Column <= sLine.Length);

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

diff --git a/Source/DafnyMenu/DafnyMenuPackage.cs b/Source/DafnyMenu/DafnyMenuPackage.cs
index cb32f9fd..5481141c 100644
--- a/Source/DafnyMenu/DafnyMenuPackage.cs
+++ b/Source/DafnyMenu/DafnyMenuPackage.cs
@@ -238,6 +238,7 @@ namespace DafnyLanguage.DafnyMenu
         if (selectedError != null)

         {

           BvdToolWindow.BVD.ReadModel(selectedError.Model);

+          BvdToolWindow.BVD.SetState(selectedError.SelectedStateId, true);

         }

 

         IVsWindowFrame windowFrame = (IVsWindowFrame)window.Frame;