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
|
using System;
using System.Collections.Generic;
using System.ComponentModel.Composition;
using System.Linq;
using System.Windows.Media;
using Microsoft.VisualStudio.Text;
using Microsoft.VisualStudio.Text.Classification;
using Microsoft.VisualStudio.Text.Editor;
using Microsoft.VisualStudio.Text.Operations;
using Microsoft.VisualStudio.Text.Tagging;
using Microsoft.VisualStudio.Utilities;
namespace DafnyLanguage
{
#if LATER_MAYBE
#region (the current annoying) word highligher
internal class HighlightWordTagger : ITagger<HighlightWordTag>
{
ITextView View { get; set; }
ITextBuffer SourceBuffer { get; set; }
ITextSearchService TextSearchService { get; set; }
ITextStructureNavigator TextStructureNavigator { get; set; }
NormalizedSnapshotSpanCollection WordSpans { get; set; }
SnapshotSpan? CurrentWord { get; set; }
SnapshotPoint RequestedPoint { get; set; }
object updateLock = new object();
public HighlightWordTagger(ITextView view, ITextBuffer sourceBuffer, ITextSearchService textSearchService,
ITextStructureNavigator textStructureNavigator) {
this.View = view;
this.SourceBuffer = sourceBuffer;
this.TextSearchService = textSearchService;
this.TextStructureNavigator = textStructureNavigator;
this.WordSpans = new NormalizedSnapshotSpanCollection();
this.CurrentWord = null;
this.View.Caret.PositionChanged += CaretPositionChanged;
this.View.LayoutChanged += ViewLayoutChanged;
}
void ViewLayoutChanged(object sender, TextViewLayoutChangedEventArgs e) {
// If a new snapshot wasn't generated, then skip this layout
if (e.NewSnapshot != e.OldSnapshot) {
UpdateAtCaretPosition(View.Caret.Position);
}
}
void CaretPositionChanged(object sender, CaretPositionChangedEventArgs e) {
UpdateAtCaretPosition(e.NewPosition);
}
public event EventHandler<SnapshotSpanEventArgs> TagsChanged;
void UpdateAtCaretPosition(CaretPosition caretPosition) {
SnapshotPoint? point = caretPosition.Point.GetPoint(SourceBuffer, caretPosition.Affinity);
if (!point.HasValue)
return;
// If the new caret position is still within the current word (and on the same snapshot), we don't need to check it
if (CurrentWord.HasValue
&& CurrentWord.Value.Snapshot == View.TextSnapshot
&& CurrentWord.Value.Start <= point.Value && point.Value <= CurrentWord.Value.End) {
return;
}
RequestedPoint = point.Value;
UpdateWordAdornments();
}
void UpdateWordAdornments() {
SnapshotPoint currentRequest = RequestedPoint;
List<SnapshotSpan> wordSpans = new List<SnapshotSpan>();
//Find all words in the buffer like the one the caret is on
TextExtent word = TextStructureNavigator.GetExtentOfWord(currentRequest);
bool foundWord = true;
//If we've selected something not worth highlighting, we might have missed a "word" by a little bit
if (!WordExtentIsValid(currentRequest, word)) {
//Before we retry, make sure it is worthwhile
if (word.Span.Start != currentRequest
|| currentRequest == currentRequest.GetContainingLine().Start
|| char.IsWhiteSpace((currentRequest - 1).GetChar())) {
foundWord = false;
} else {
// Try again, one character previous.
//If the caret is at the end of a word, pick up the word.
word = TextStructureNavigator.GetExtentOfWord(currentRequest - 1);
//If the word still isn't valid, we're done
if (!WordExtentIsValid(currentRequest, word))
foundWord = false;
}
}
if (!foundWord) {
//If we couldn't find a word, clear out the existing markers
SynchronousUpdate(currentRequest, new NormalizedSnapshotSpanCollection(), null);
return;
}
SnapshotSpan currentWord = word.Span;
//If this is the current word, and the caret moved within a word, we're done.
if (CurrentWord.HasValue && currentWord == CurrentWord)
return;
//Find the new spans
FindData findData = new FindData(currentWord.GetText(), currentWord.Snapshot);
findData.FindOptions = FindOptions.WholeWord | FindOptions.MatchCase;
wordSpans.AddRange(TextSearchService.FindAll(findData));
//If another change hasn't happened, do a real update
if (currentRequest == RequestedPoint)
SynchronousUpdate(currentRequest, new NormalizedSnapshotSpanCollection(wordSpans), currentWord);
}
static bool WordExtentIsValid(SnapshotPoint currentRequest, TextExtent word) {
return word.IsSignificant
&& currentRequest.Snapshot.GetText(word.Span).Any(c => char.IsLetter(c));
}
void SynchronousUpdate(SnapshotPoint currentRequest, NormalizedSnapshotSpanCollection newSpans, SnapshotSpan? newCurrentWord) {
lock (updateLock) {
if (currentRequest != RequestedPoint)
return;
WordSpans = newSpans;
CurrentWord = newCurrentWord;
var chngd = TagsChanged;
if (chngd != null)
chngd(this, new SnapshotSpanEventArgs(new SnapshotSpan(SourceBuffer.CurrentSnapshot, 0, SourceBuffer.CurrentSnapshot.Length)));
}
}
public IEnumerable<ITagSpan<HighlightWordTag>> GetTags(NormalizedSnapshotSpanCollection spans) {
if (CurrentWord == null)
yield break;
// Hold on to a "snapshot" of the word spans and current word, so that we maintain the same
// collection throughout
SnapshotSpan currentWord = CurrentWord.Value;
NormalizedSnapshotSpanCollection wordSpans = WordSpans;
if (spans.Count == 0 || WordSpans.Count == 0)
yield break;
// If the requested snapshot isn't the same as the one our words are on, translate our spans to the expected snapshot
if (spans[0].Snapshot != wordSpans[0].Snapshot) {
wordSpans = new NormalizedSnapshotSpanCollection(
wordSpans.Select(span => span.TranslateTo(spans[0].Snapshot, SpanTrackingMode.EdgeExclusive)));
currentWord = currentWord.TranslateTo(spans[0].Snapshot, SpanTrackingMode.EdgeExclusive);
}
// First, yield back the word the cursor is under (if it overlaps)
// Note that we'll yield back the same word again in the wordspans collection;
// the duplication here is expected.
if (spans.OverlapsWith(new NormalizedSnapshotSpanCollection(currentWord)))
yield return new TagSpan<HighlightWordTag>(currentWord, new HighlightWordTag());
// Second, yield all the other words in the file
foreach (SnapshotSpan span in NormalizedSnapshotSpanCollection.Overlap(spans, wordSpans)) {
yield return new TagSpan<HighlightWordTag>(span, new HighlightWordTag());
}
}
}
internal class HighlightWordTag : TextMarkerTag
{
public HighlightWordTag() : base("MarkerFormatDefinition/HighlightWordFormatDefinition") { }
}
[Export(typeof(EditorFormatDefinition))]
[Name("MarkerFormatDefinition/HighlightWordFormatDefinition")]
[UserVisible(true)]
internal class HighlightWordFormatDefinition : MarkerFormatDefinition
{
public HighlightWordFormatDefinition() {
this.BackgroundColor = Colors.LightBlue;
this.ForegroundColor = Colors.DarkBlue;
this.DisplayName = "Highlight Word";
this.ZOrder = 5;
}
}
[Export(typeof(IViewTaggerProvider))]
[ContentType("text")]
[TagType(typeof(TextMarkerTag))]
internal class HighlightWordTaggerProvider : IViewTaggerProvider
{
[Import]
internal ITextSearchService TextSearchService { get; set; }
[Import]
internal ITextStructureNavigatorSelectorService TextStructureNavigatorSelector { get; set; }
public ITagger<T> CreateTagger<T>(ITextView textView, ITextBuffer buffer) where T : ITag {
//provide highlighting only on the top buffer
if (textView.TextBuffer != buffer)
return null;
ITextStructureNavigator textStructureNavigator =
TextStructureNavigatorSelector.GetTextStructureNavigator(buffer);
return new HighlightWordTagger(textView, buffer, TextSearchService, textStructureNavigator) as ITagger<T>;
}
}
#endregion
#endif
}
|
