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
|
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Text.RegularExpressions;
using System.Windows.Threading;
using System.ComponentModel.Composition;
using Microsoft.VisualStudio.Text.Outlining;
using Microsoft.VisualStudio.Text.Tagging;
using Microsoft.VisualStudio.Utilities;
using Microsoft.VisualStudio.Text;
namespace DafnyLanguage
{
#if THIS_IS_THE_PAST
[Export(typeof(ITaggerProvider))]
[ContentType("dafny")]
[TagType(typeof(IOutliningRegionTag))]
internal sealed class OutliningTaggerProvider : ITaggerProvider
{
public ITagger<T> CreateTagger<T>(ITextBuffer buffer) where T : ITag {
// create a single tagger for each buffer.
Func<ITagger<T>> sc = delegate() { return new OutlineTagger(buffer) as ITagger<T>; };
return buffer.Properties.GetOrCreateSingletonProperty<ITagger<T>>(sc);
}
}
/// <summary>
/// Data about one outline region
/// </summary>
internal class OutlineRegion
{
public SnapshotPoint Start { get; set; }
public SnapshotPoint End { get; set; }
public SnapshotSpan Span {
get { return new SnapshotSpan(Start, End); }
}
public string HoverText { get; set; }
public string Label { get; set; }
}
internal sealed class OutlineTagger : ITagger<IOutliningRegionTag>
{
ITextBuffer _buffer;
ITextSnapshot _snapshot;
List<OutlineRegion> _regions;
public OutlineTagger(ITextBuffer buffer) {
_buffer = buffer;
_snapshot = buffer.CurrentSnapshot;
_regions = new List<OutlineRegion>();
ReparseFile(null, EventArgs.Empty);
// listen for changes to the buffer, but don't process until the user stops typing
BufferIdleEventUtil.AddBufferIdleEventListener(_buffer, ReparseFile);
}
public void Dispose() {
BufferIdleEventUtil.RemoveBufferIdleEventListener(_buffer, ReparseFile);
}
public IEnumerable<ITagSpan<IOutliningRegionTag>> GetTags(NormalizedSnapshotSpanCollection spans) {
if (spans.Count == 0)
yield break;
List<OutlineRegion> currentRegions = _regions;
ITextSnapshot currentSnapshot = _snapshot;
// 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 outline tags for any regions that fall within that span
foreach (var region in currentRegions) {
if (entire.IntersectsWith(region.Span)) {
//the region starts at the beginning of the "{", and goes until the *end* of the line that contains the "}".
yield return new TagSpan<OutliningRegionTag>(new SnapshotSpan(region.Start, region.End),
new OutliningRegionTag(false, false, region.Label, region.HoverText));
}
}
}
public event EventHandler<SnapshotSpanEventArgs> TagsChanged;
static string ellipsis = "..."; //the characters that are displayed when the region is collapsed
static Regex matchKey = new Regex("^\\s*(datatype|method|function)");
static int MaxHiddenLines = 15;
static char[] eitherBrace = { '{', '}' };
/// <summary>
/// Find all of the outline sections in the snapshot
/// </summary>
private List<OutlineRegion> ParseOutlineSections(ITextSnapshot newSnapshot) {
List<OutlineRegion> newRegions = new List<OutlineRegion>();
// We care about three states:
// (0) looking for an outlineable declaration
// (1) have found an outlineable declaration, looking for an open curly
// (2) looking for a close curly
// The search used here is not at all exact, and it would be easy to get it to
// do the wrong thing; however, in common cases, it will do the right thing.
int state = 0;
SnapshotPoint start = new SnapshotPoint(); // the value of "start" matters only if state==2
int braceImbalance = 0; // used only if state==2
string hoverText = ""; // used only if state==2
int hoverLineCount = 0; // used only if state==2
string prevLineBreak = ""; // used only if state==2
foreach (ITextSnapshotLine line in newSnapshot.Lines) {
string txt = line.GetText();
if (state == 0) {
MatchCollection matches = matchKey.Matches(txt);
if (matches.Count != 0)
state = 1;
}
int startPos = 0;
if (state == 1) {
startPos = txt.IndexOf('{');
if (startPos != -1) {
start = new SnapshotPoint(newSnapshot, line.Start.Position + startPos + 1);
startPos++;
state = 2;
braceImbalance = 1;
hoverText = txt.Substring(startPos).Trim();
hoverLineCount = hoverText.Length == 0 ? 0 : 1;
prevLineBreak = line.GetLineBreakText();
}
}
if (state == 2) {
int endPos = startPos;
while (braceImbalance != 0) {
endPos = txt.IndexOfAny(eitherBrace, endPos);
if (endPos == -1) break;
char ch = txt[endPos];
if (ch == '{') {
braceImbalance++;
} else {
braceImbalance--;
if (braceImbalance == 0) break;
}
endPos++;
}
if (endPos == -1) {
// not there yet
if (startPos == 0 && hoverLineCount < MaxHiddenLines) {
string h = txt.Trim();
if (h.Length != 0) {
if (hoverText.Length != 0)
hoverText += prevLineBreak;
hoverText += h;
hoverLineCount++;
prevLineBreak = line.GetLineBreakText();
}
}
} else {
// we found the end
if (startPos != 0) {
hoverText = txt.Substring(startPos, endPos - startPos).Trim();
} else if (hoverLineCount < MaxHiddenLines) {
string h = txt.Substring(0, endPos).Trim();
if (h.Length != 0) {
if (hoverText.Length != 0)
hoverText += prevLineBreak;
hoverText += h;
}
}
SnapshotPoint end = new SnapshotPoint(newSnapshot, line.Start.Position + endPos);
newRegions.Add(new OutlineRegion() {
Start = start, End = end, Label = ellipsis,
HoverText = hoverText
});
state = 0;
}
}
}
return newRegions;
}
/// <summary>
/// Find all of the outline regions in the document (snapshot) and notify
/// listeners of any that changed
/// </summary>
void ReparseFile(object sender, EventArgs args) {
ITextSnapshot snapshot = _buffer.CurrentSnapshot;
// get all of the outline regions in the snapshot
List<OutlineRegion> newRegions = ParseOutlineSections(snapshot);
// determine the changed span, and send a changed event with the new spans
List<SnapshotSpan> oldSpans = new List<SnapshotSpan>(_regions.Select(r =>
r.Span.TranslateTo(snapshot, SpanTrackingMode.EdgeExclusive)));
List<SnapshotSpan> newSpans = new List<SnapshotSpan>(newRegions.Select(r => r.Span));
NormalizedSnapshotSpanCollection oldSpanCollection = new NormalizedSnapshotSpanCollection(oldSpans);
NormalizedSnapshotSpanCollection newSpanCollection = new NormalizedSnapshotSpanCollection(newSpans);
NormalizedSnapshotSpanCollection difference = SymmetricDifference(oldSpanCollection, newSpanCollection);
// save the new baseline
_snapshot = snapshot;
_regions = newRegions;
foreach (var span in difference) {
var chng = TagsChanged;
if (chng != null)
chng(this, new SnapshotSpanEventArgs(span));
}
}
NormalizedSnapshotSpanCollection SymmetricDifference(NormalizedSnapshotSpanCollection first, NormalizedSnapshotSpanCollection second) {
return NormalizedSnapshotSpanCollection.Union(
NormalizedSnapshotSpanCollection.Difference(first, second),
NormalizedSnapshotSpanCollection.Difference(second, first));
}
}
#endif
}
|
