DafnyExtension: improvements

4 files changed, 17 insertions, 231 deletions

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj
index 62413d03..cfa7a070 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj
@@ -135,7 +135,6 @@
     <Compile Include="ContentType.cs" />

     <Compile Include="BraceMatching.cs" />

     <Compile Include="WordHighlighter.cs" />

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

     <Compile Include="ErrorTagger.cs" />

     <Compile Include="TokenTagger.cs" />

     <Compile Include="ClassificationTagger.cs" />

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/Outlining.cs b/Util/VS2010/DafnyExtension/DafnyExtension/Outlining.cs
deleted file mode 100644
index 3e64e43d..00000000
--- a/Util/VS2010/DafnyExtension/DafnyExtension/Outlining.cs
+++ /dev/null
@@ -1,222 +0,0 @@
-using System;

-using System.Collections.Generic;

-using System.Linq;

-using System.Text;

-using System.Text.RegularExpressions;

-using System.Windows.Threading;

-using System.ComponentModel.Composition;

-using Microsoft.VisualStudio.Text.Outlining;

-using Microsoft.VisualStudio.Text.Tagging;

-using Microsoft.VisualStudio.Utilities;

-using Microsoft.VisualStudio.Text;

-

-namespace DafnyLanguage

-{

-#if THIS_IS_THE_PAST

-  [Export(typeof(ITaggerProvider))]

-  [ContentType("dafny")]

-  [TagType(typeof(IOutliningRegionTag))]

-  internal sealed class OutliningTaggerProvider : ITaggerProvider

-  {

-    public ITagger<T> CreateTagger<T>(ITextBuffer buffer) where T : ITag {

-      // create a single tagger for each buffer.

-      Func<ITagger<T>> sc = delegate() { return new OutlineTagger(buffer) as ITagger<T>; };

-      return buffer.Properties.GetOrCreateSingletonProperty<ITagger<T>>(sc);

-    }

-  }

-

-  /// <summary>

-  /// Data about one outline region

-  /// </summary>

-  internal class OutlineRegion

-  {

-    public SnapshotPoint Start { get; set; }

-    public SnapshotPoint End { get; set; }

-    public SnapshotSpan Span {

-      get { return new SnapshotSpan(Start, End); }

-    }

-

-    public string HoverText { get; set; }

-    public string Label { get; set; }

-  }

-

-  internal sealed class OutlineTagger : ITagger<IOutliningRegionTag>

-  {

-    ITextBuffer _buffer;

-    ITextSnapshot _snapshot;

-    List<OutlineRegion> _regions;

-

-    public OutlineTagger(ITextBuffer buffer) {

-      _buffer = buffer;

-      _snapshot = buffer.CurrentSnapshot;

-      _regions = new List<OutlineRegion>();

-

-      ReparseFile(null, EventArgs.Empty);

-

-      // listen for changes to the buffer, but don't process until the user stops typing

-      BufferIdleEventUtil.AddBufferIdleEventListener(_buffer, ReparseFile);

-    }

-

-    public void Dispose() {

-      BufferIdleEventUtil.RemoveBufferIdleEventListener(_buffer, ReparseFile);

-    }

-

-    public IEnumerable<ITagSpan<IOutliningRegionTag>> GetTags(NormalizedSnapshotSpanCollection spans) {

-      if (spans.Count == 0)

-        yield break;

-

-      List<OutlineRegion> currentRegions = _regions;

-      ITextSnapshot currentSnapshot = _snapshot;

-

-      // create a new SnapshotSpan for the entire region encompassed by the span collection

-      SnapshotSpan entire = new SnapshotSpan(spans[0].Start, spans[spans.Count - 1].End).TranslateTo(currentSnapshot, SpanTrackingMode.EdgeExclusive);

-      int startLineNumber = entire.Start.GetContainingLine().LineNumber;

-      int endLineNumber = entire.End.GetContainingLine().LineNumber;

-

-      // return outline tags for any regions that fall within that span

-      foreach (var region in currentRegions) {

-        if (entire.IntersectsWith(region.Span)) {

-          //the region starts at the beginning of the "{", and goes until the *end* of the line that contains the "}".

-          yield return new TagSpan<OutliningRegionTag>(new SnapshotSpan(region.Start, region.End),

-            new OutliningRegionTag(false, false, region.Label, region.HoverText));

-        }

-      }

-    }

-

-    public event EventHandler<SnapshotSpanEventArgs> TagsChanged;

-

-    static string ellipsis = "...";    //the characters that are displayed when the region is collapsed

-    static Regex matchKey = new Regex("^\\s*(datatype|method|function)");

-    static int MaxHiddenLines = 15;

-    static char[] eitherBrace = { '{', '}' };

-

-    /// <summary>

-    /// Find all of the outline sections in the snapshot

-    /// </summary>

-    private List<OutlineRegion> ParseOutlineSections(ITextSnapshot newSnapshot) {

-      List<OutlineRegion> newRegions = new List<OutlineRegion>();

-

-      // We care about three states:

-      // (0) looking for an outlineable declaration

-      // (1) have found an outlineable declaration, looking for an open curly

-      // (2) looking for a close curly

-      // The search used here is not at all exact, and it would be easy to get it to

-      // do the wrong thing; however, in common cases, it will do the right thing.

-      int state = 0;

-      SnapshotPoint start = new SnapshotPoint();  // the value of "start" matters only if state==2

-      int braceImbalance = 0;  // used only if state==2

-      string hoverText = "";  // used only if state==2

-      int hoverLineCount = 0;  // used only if state==2

-      string prevLineBreak = "";  // used only if state==2

-      foreach (ITextSnapshotLine line in newSnapshot.Lines) {

-        string txt = line.GetText();

-        if (state == 0) {

-          MatchCollection matches = matchKey.Matches(txt);

-          if (matches.Count != 0)

-            state = 1;

-        }

-        int startPos = 0;

-        if (state == 1) {

-          startPos = txt.IndexOf('{');

-          if (startPos != -1) {

-            start = new SnapshotPoint(newSnapshot, line.Start.Position + startPos + 1);

-            startPos++;

-            state = 2;

-            braceImbalance = 1;

-            hoverText = txt.Substring(startPos).Trim();

-            hoverLineCount = hoverText.Length == 0 ? 0 : 1;

-            prevLineBreak = line.GetLineBreakText();

-          }

-        }

-        if (state == 2) {

-          int endPos = startPos;

-          while (braceImbalance != 0) {

-            endPos = txt.IndexOfAny(eitherBrace, endPos);

-            if (endPos == -1) break;

-            char ch = txt[endPos];

-            if (ch == '{') {

-              braceImbalance++;

-            } else {

-              braceImbalance--;

-              if (braceImbalance == 0) break;

-            }

-            endPos++;

-          }

-

-          if (endPos == -1) {

-            // not there yet

-            if (startPos == 0 && hoverLineCount < MaxHiddenLines) {

-              string h = txt.Trim();

-              if (h.Length != 0) {

-                if (hoverText.Length != 0)

-                  hoverText += prevLineBreak;

-                hoverText += h;

-                hoverLineCount++;

-                prevLineBreak = line.GetLineBreakText();

-              }

-            }

-          } else {

-            // we found the end

-            if (startPos != 0) {

-              hoverText = txt.Substring(startPos, endPos - startPos).Trim();

-            } else if (hoverLineCount < MaxHiddenLines) {

-              string h = txt.Substring(0, endPos).Trim();

-              if (h.Length != 0) {

-                if (hoverText.Length != 0)

-                  hoverText += prevLineBreak;

-                hoverText += h;

-              }

-            }

-            SnapshotPoint end = new SnapshotPoint(newSnapshot, line.Start.Position + endPos);

-            newRegions.Add(new OutlineRegion() {

-              Start = start, End = end, Label = ellipsis,

-              HoverText = hoverText

-            });

-            state = 0;

-          }

-        }

-      }

-

-      return newRegions;

-    }

-

-    /// <summary>

-    /// Find all of the outline regions in the document (snapshot) and notify

-    /// listeners of any that changed

-    /// </summary>

-    void ReparseFile(object sender, EventArgs args) {

-      ITextSnapshot snapshot = _buffer.CurrentSnapshot;

-

-      // get all of the outline regions in the snapshot

-      List<OutlineRegion> newRegions = ParseOutlineSections(snapshot);

-

-      // determine the changed span, and send a changed event with the new spans

-      List<SnapshotSpan> oldSpans = new List<SnapshotSpan>(_regions.Select(r =>

-        r.Span.TranslateTo(snapshot, SpanTrackingMode.EdgeExclusive)));

-

-      List<SnapshotSpan> newSpans = new List<SnapshotSpan>(newRegions.Select(r => r.Span));

-

-      NormalizedSnapshotSpanCollection oldSpanCollection = new NormalizedSnapshotSpanCollection(oldSpans);

-      NormalizedSnapshotSpanCollection newSpanCollection = new NormalizedSnapshotSpanCollection(newSpans);

-

-      NormalizedSnapshotSpanCollection difference = SymmetricDifference(oldSpanCollection, newSpanCollection);

-

-      // save the new baseline

-      _snapshot = snapshot;

-      _regions = newRegions;

-

-      foreach (var span in difference) {

-        var chng = TagsChanged;

-        if (chng != null)

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

-      }

-    }

-

-    NormalizedSnapshotSpanCollection SymmetricDifference(NormalizedSnapshotSpanCollection first, NormalizedSnapshotSpanCollection second) {

-      return NormalizedSnapshotSpanCollection.Union(

-          NormalizedSnapshotSpanCollection.Difference(first, second),

-          NormalizedSnapshotSpanCollection.Difference(second, first));

-    }

-  }

-#endif

-}

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs
index 8cbdb9f6..86a53460 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs
@@ -119,7 +119,7 @@ namespace DafnyLanguage
           newRegions.Add(new ORegion(module, "module"));

         }

         foreach (Dafny.TopLevelDecl d in module.TopLevelDecls) {

-          if (!HasBodyTokens(d)) {

+          if (!HasBodyTokens(d) && !(d is Dafny.ClassDecl)) {

             continue;

           }

           if (d is Dafny.ArbitraryTypeDecl) {

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs
index fcc31a3c..10bb36e1 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs
@@ -102,6 +102,10 @@ namespace DafnyLanguage
       foreach (var err in _resolutionErrors) {

         yield return err;

       }

+      if (_resolutionErrors.Count != 0) {

+        // we're done

+        yield break;

+      }

       foreach (var err in _verificationErrors) {

         yield return err;

       }

@@ -112,14 +116,10 @@ namespace DafnyLanguage
     /// </summary>

     public IEnumerable<ITagSpan<DafnyResolverTag>> GetTags(NormalizedSnapshotSpanCollection spans) {

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

+      var currentSnapshot = spans[0].Snapshot;

       foreach (var err in AllErrors()) {

         if (err.Category != ErrorCategory.ProcessError) {

-          Contract.Assert(0 <= err.Line);

-          var line = _snapshot.GetLineFromLineNumber(err.Line);

-          Contract.Assert(err.Column <= line.Length);

-          var length = line.Length - err.Column;

-          if (5 < length) length = 5;

-          var span = new SnapshotSpan(new SnapshotPoint(_snapshot, line.Start.Position + err.Column), length);

+          var span = err.Span().TranslateTo(currentSnapshot, SpanTrackingMode.EdgeExclusive);

           string ty;  // the COLORs below indicate what I see on my machine

           switch (err.Category) {

             default:  // unexpected category

@@ -282,13 +282,15 @@ namespace DafnyLanguage
   {

     public readonly int Line;  // 0 based

     public readonly int Column;  // 0 based

-    public ITextSnapshot Snapshot;  // filled in during the FillInSnapshot call

+    ITextSnapshot Snapshot;  // filled in during the FillInSnapshot call

     public readonly ErrorCategory Category;

     public readonly string Message;

     /// <summary>

     /// "line" and "col" are expected to be 0-based

     /// </summary>

     public DafnyError(int line, int col, ErrorCategory cat, string msg) {

+      Contract.Requires(0 <= line);

+      Contract.Requires(0 <= col);

       Line = line;

       Column = col;

       Category = cat;

@@ -299,5 +301,12 @@ namespace DafnyLanguage
       Contract.Requires(snapshot != null);

       Snapshot = snapshot;

     }

+    public SnapshotSpan Span() {

+      Contract.Requires(Snapshot != null);  // requires that Snapshot has been filled in

+      var line = Snapshot.GetLineFromLineNumber(Line);

+      Contract.Assume(Column <= line.Length);  // this is really a precondition of the constructor + FillInSnapshot

+      var length = Math.Min(line.Length - Column, 5);

+      return new SnapshotSpan(line.Start + Column, length);

+    }

   }

 }