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
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
|
//***************************************************************************
// 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 System;
using System.Collections.Generic;
using System.ComponentModel.Composition;
using System.Diagnostics.Contracts;
using Microsoft.VisualStudio.Text;
using Microsoft.VisualStudio.Text.Tagging;
using Microsoft.VisualStudio.Utilities;
using Bpl = Microsoft.Boogie;
using Dafny = Microsoft.Dafny;
namespace DafnyLanguage
{
#region Provider
[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<IDafnyResolverTag> tagAggregator = AggregatorFactory.CreateTagAggregator<IDafnyResolverTag>(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);
}
}
#endregion
#region Tagger
/// <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<OutliningRegion> _regions = new List<OutliningRegion>(); // the regions generated from _program
ITagAggregator<IDafnyResolverTag> _aggregator;
internal OutliningTagger(ITextBuffer buffer, ITagAggregator<IDafnyResolverTag> 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<OutliningRegion> newRegions = new List<OutliningRegion>();
foreach (var module in program.Modules) {
if (!module.IsDefaultModule) {
var nm = "module";
if (module.IsAbstract) {
nm = "abstract " + nm;
}
OutliningRegion.Add(newRegions, program, module, nm);
}
foreach (Dafny.TopLevelDecl d in module.TopLevelDecls) {
if (!HasBodyTokens(d) && !(d is Dafny.ClassDecl)) {
continue;
}
if (d is Dafny.OpaqueTypeDecl) {
OutliningRegion.Add(newRegions, program, d, "type");
} else if (d is Dafny.CoDatatypeDecl) {
OutliningRegion.Add(newRegions, program, d, "codatatype");
} else if (d is Dafny.DatatypeDecl) {
OutliningRegion.Add(newRegions, program, d, "datatype");
} else if (d is Dafny.ModuleDecl) {
// do nothing here, since the outer loop handles modules
} else {
var cl = (Dafny.ClassDecl)d;
if (cl.IsDefaultClass) {
// do nothing
} else if (cl is Dafny.IteratorDecl) {
OutliningRegion.Add(newRegions, program, cl, "iterator");
} else {
OutliningRegion.Add(newRegions, program, 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) {
var nm =
m is Dafny.InductivePredicate ? "inductive predicate" :
m is Dafny.CoPredicate ? "copredicate" :
// m is Dafny.PrefixPredicate ? "prefix predicate" : // this won't ever occur here
m is Dafny.Predicate ? "predicate" :
"function";
if (!m.IsGhost) {
nm += " method";
}
OutliningRegion.Add(newRegions, program, m, nm);
} else if (m is Dafny.Method && ((Dafny.Method)m).Body != null) {
var nm =
m is Dafny.Constructor ? "constructor" :
m is Dafny.CoLemma ? "colemma" :
m is Dafny.Lemma ? "lemma" :
// m is Dafny.PrefixLemma ? "prefix lemma" : // this won't ever occur here
"method";
if (m.IsGhost && !(m is Dafny.CoLemma)) {
nm = "ghost " + nm;
}
OutliningRegion.Add(newRegions, program, m, nm);
}
}
}
}
}
_snapshot = snapshot;
_regions = newRegions;
_program = program;
return true;
}
static bool HasBodyTokens(Dafny.Declaration decl) {
Contract.Requires(decl != null);
return decl.BodyStartTok != Bpl.Token.NoToken && decl.BodyEndTok != Bpl.Token.NoToken;
}
class OutliningRegion : DafnyRegion
{
public static void Add(List<OutliningRegion> regions, Microsoft.Dafny.Program prog, Dafny.INamedRegion decl, string kind) {
Contract.Requires(regions != null);
Contract.Requires(prog != null);
if (InMainFileAndUserDefined(prog, decl.BodyStartTok)) {
regions.Add(new OutliningRegion(decl, kind));
}
}
public readonly int Start;
public readonly int Length;
public readonly string HoverText;
private OutliningRegion(Dafny.INamedRegion 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);
}
}
}
#endregion
}
|
