Dafny: added Statement.SubExpressions getter

DafnyExtension: added hover text for identifiers

1 files changed, 6 insertions, 15 deletions

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
index 3e6d944f..c4ba346a 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
@@ -24,27 +24,21 @@ namespace DafnyLanguage
   public enum DafnyTokenKinds

   {

     Keyword, Number, String, Comment,

-    TypeIdentifier, VariableIdentifier

+    VariableIdentifier, VariableIdentifierDefinition

   }

 

   public class DafnyTokenTag : ITag

   {

     public DafnyTokenKinds Kind { get; private set; }

+    public string HoverText { get; private set; }

 

     public DafnyTokenTag(DafnyTokenKinds kind) {

       this.Kind = kind;

     }

-  }

-  public class IdentifierDafnyTokenTag : DafnyTokenTag

-  {

-    public IdentifierDafnyTokenTag()

-      : base(DafnyTokenKinds.VariableIdentifier) {

-    }

-  }

-  public class TypeDafnyTokenTag : DafnyTokenTag

-  {

-    public TypeDafnyTokenTag()

-      : base(DafnyTokenKinds.TypeIdentifier) {

+

+    public DafnyTokenTag(DafnyTokenKinds kind, string hoverText) {

+      this.Kind = kind;

+      this.HoverText = hoverText;

     }

   }

 

@@ -73,14 +67,11 @@ namespace DafnyLanguage
 

       // 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 tags for any regions that fall within that span

       // BUGBUG: depending on how GetTags gets called (e.g., once for each line in the buffer), this may produce quadratic behavior

       foreach (var region in currentRegions) {

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

-          // BUGBUG: this returns a span for currentSnapshot, but shouldn't we return spans for the spans[0].Snapshot?

           yield return new TagSpan<DafnyTokenTag>(new SnapshotSpan(region.Start, region.End), new DafnyTokenTag(region.Kind));

         }

       }