1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
|
//***************************************************************************
// 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 EnvDTE;
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.ComponentModel.Composition;
using System.Windows.Threading;
using Microsoft.VisualStudio.Shell;
using Microsoft.VisualStudio.Shell.Interop;
using Microsoft.VisualStudio.Text;
using Microsoft.VisualStudio.Text.Classification;
using Microsoft.VisualStudio.Text.Editor;
using Microsoft.VisualStudio.Text.Tagging;
using Microsoft.VisualStudio.Text.Projection;
using Microsoft.VisualStudio.Utilities;
using System.Diagnostics.Contracts;
using Bpl = Microsoft.Boogie;
using Dafny = Microsoft.Dafny;
namespace DafnyLanguage
{
[Export(typeof(ITaggerProvider))]
[ContentType("dafny")]
[TagType(typeof(IOutliningRegionTag))]
internal sealed class OutliningTaggerProvider : ITaggerProvider
{
[Import]
internal IBufferTagAggregatorFactoryService AggregatorFactory = null;
public ITagger<T> CreateTagger<T>(ITextBuffer buffer) where T : ITag {
ITagAggregator<DafnyResolverTag> tagAggregator = AggregatorFactory.CreateTagAggregator<DafnyResolverTag>(buffer);
// create a single tagger for each buffer.
Func<ITagger<T>> sc = delegate() { return new OutliningTagger(buffer, tagAggregator) as ITagger<T>; };
return buffer.Properties.GetOrCreateSingletonProperty<ITagger<T>>(sc);
}
}
/// <summary>
/// Translate DafnyResolverTag's into IOutliningRegionTag's
/// </summary>
internal sealed class OutliningTagger : ITagger<IOutliningRegionTag>
{
ITextBuffer _buffer;
ITextSnapshot _snapshot; // the most recent snapshot of _buffer that we have been informed about
Dafny.Program _program; // the program parsed from _snapshot
List<ORegion> _regions = new List<ORegion>(); // the regions generated from _program
ITagAggregator<DafnyResolverTag> _aggregator;
internal OutliningTagger(ITextBuffer buffer, ITagAggregator<DafnyResolverTag> tagAggregator) {
_buffer = buffer;
_snapshot = _buffer.CurrentSnapshot;
_aggregator = tagAggregator;
_aggregator.TagsChanged += new EventHandler<TagsChangedEventArgs>(_aggregator_TagsChanged);
}
/// <summary>
/// Find the Error tokens in the set of all tokens and create an ErrorTag for each
/// </summary>
public IEnumerable<ITagSpan<IOutliningRegionTag>> GetTags(NormalizedSnapshotSpanCollection spans) {
if (spans.Count == 0) yield break;
// (A NormalizedSnapshotSpanCollection contains spans that all come from the same snapshot.)
// The spans are ordered by the .Start component, and the collection contains no adjacent or abutting spans.
// Hence, to find a span that includes all the ones in "spans", we only need to look at the .Start for the
// first spand and the .End of the last span:
var startPoint = spans[0].Start;
var endPoint = spans[spans.Count - 1].End;
// Note, (startPoint,endPoint) are points in the spans for which we're being asked to provide tags. We need to translate
// these back into the most recent snapshot that we've computed regions for, namely _snapshot.
var entire = new SnapshotSpan(startPoint, endPoint).TranslateTo(_snapshot, SpanTrackingMode.EdgeExclusive);
int start = entire.Start;
int end = entire.End;
if (start == end) yield break;
foreach (var r in _regions) {
if (0 <= r.Length && r.Start <= end && start <= r.Start + r.Length) {
yield return new TagSpan<OutliningRegionTag>(
new SnapshotSpan(_snapshot, r.Start, r.Length),
new OutliningRegionTag(false, false, "...", r.HoverText));
}
}
}
// the Classifier tagger is translating buffer change events into TagsChanged events, so we don't have to
public event EventHandler<SnapshotSpanEventArgs> TagsChanged;
void _aggregator_TagsChanged(object sender, TagsChangedEventArgs e) {
var r = sender as ResolverTagger;
if (r != null) {
ITextSnapshot snap;
Microsoft.Dafny.Program prog;
lock (this) {
snap = r._snapshot;
prog = r._program;
}
if (prog != null) {
if (!ComputeOutliningRegions(prog, snap))
return; // no new regions
var chng = TagsChanged;
if (chng != null) {
NormalizedSnapshotSpanCollection spans = e.Span.GetSpans(_buffer.CurrentSnapshot);
if (spans.Count > 0) {
SnapshotSpan span = new SnapshotSpan(spans[0].Start, spans[spans.Count - 1].End);
chng(this, new SnapshotSpanEventArgs(span));
}
}
}
}
}
bool ComputeOutliningRegions(Dafny.Program program, ITextSnapshot snapshot) {
Contract.Requires(snapshot != null);
if (program == _program)
return false; // no new regions
List<ORegion> newRegions = new List<ORegion>();
foreach (var module in program.Modules) {
if (!module.IsDefaultModule) {
newRegions.Add(new ORegion(module, "module"));
}
foreach (Dafny.TopLevelDecl d in module.TopLevelDecls) {
if (!HasBodyTokens(d) && !(d is Dafny.ClassDecl)) {
continue;
}
if (d is Dafny.ArbitraryTypeDecl) {
newRegions.Add(new ORegion(d, "type"));
} else if (d is Dafny.CoDatatypeDecl) {
newRegions.Add(new ORegion(d, "codatatype"));
} else if (d is Dafny.DatatypeDecl) {
newRegions.Add(new ORegion(d, "datatype"));
} else if (d is Dafny.ModuleDecl) {
// do nothing here, since the outer loop handles modules
} else {
Dafny.ClassDecl cl = (Dafny.ClassDecl)d;
if (!cl.IsDefaultClass) {
newRegions.Add(new ORegion(cl, "class"));
}
// do the class members (in particular, functions and methods)
foreach (Dafny.MemberDecl m in cl.Members) {
if (!HasBodyTokens(m)) {
continue;
}
if (m is Dafny.Function && ((Dafny.Function)m).Body != null) {
newRegions.Add(new ORegion(m, m is Dafny.CoPredicate ? "copredicate" : m is Dafny.Predicate ? "predicate" : "function"));
} else if (m is Dafny.Method && ((Dafny.Method)m).Body != null) {
newRegions.Add(new ORegion(m, m is Dafny.Constructor ? "constructor" : "method"));
}
}
}
}
}
_snapshot = snapshot;
_regions = newRegions;
_program = program;
return true;
}
bool HasBodyTokens(Dafny.Declaration decl) {
Contract.Requires(decl != null);
return decl.BodyStartTok != Bpl.Token.NoToken && decl.BodyEndTok != Bpl.Token.NoToken;
}
class ORegion
{
public readonly int Start;
public readonly int Length;
public readonly string HoverText;
public ORegion(Dafny.Declaration decl, string kind) {
int startPosition = decl.BodyStartTok.pos + 1; // skip the open-curly brace itself
int length = decl.BodyEndTok.pos - startPosition;
Start = startPosition;
Length = length;
HoverText = string.Format("body of {0} {1}", kind, decl.Name);
}
}
}
}
|
