diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-08-15 16:07:10 -0700 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-08-15 16:07:10 -0700 |
| commit | 10dc343a73148707fc07127ff0f88ed73f3ecf99 (patch) | |
| tree | 21610d9b6617c487648d32a1068d919935b97a33 /Util/VS2010 | |
| parent | 7ba7b6d9b4894b68ed04deab43c3d13dac302b88 (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.cs | 21 |
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));
}
}
|