summaryrefslogtreecommitdiff
path: root/Util/VS2010
diff options
context:
space:
mode:
authorGravatar Unknown <leino@LEINO6.redmond.corp.microsoft.com>2012-08-15 16:07:10 -0700
committerGravatar Unknown <leino@LEINO6.redmond.corp.microsoft.com>2012-08-15 16:07:10 -0700
commit10dc343a73148707fc07127ff0f88ed73f3ecf99 (patch)
tree21610d9b6617c487648d32a1068d919935b97a33 /Util/VS2010
parent7ba7b6d9b4894b68ed04deab43c3d13dac302b88 (diff)
Dafny: added Statement.SubExpressions getter
DafnyExtension: added hover text for identifiers
Diffstat (limited to 'Util/VS2010')
-rw-r--r--Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs21
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));
}
}