blob: 9ac9ea071f0efe85a17f6b945f55686182ed7c04 (
plain)
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
|
//***************************************************************************
// 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 Microsoft.VisualStudio.Text;
using Microsoft.VisualStudio.Text.Tagging;
using Microsoft.VisualStudio.Utilities;
namespace DafnyLanguage
{
#region Provider
[Export(typeof(ITaggerProvider))]
[Name("ErrorTagger")]
[ContentType("dafny")]
[TagType(typeof(IErrorTag))]
internal sealed class ErrorTaggerProvider : 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 ErrorTagger(buffer, tagAggregator) as ITagger<T>; };
return buffer.Properties.GetOrCreateSingletonProperty<ITagger<T>>(sc);
}
}
#endregion
#region Tagger
/// <summary>
/// Translate PkgDefTokenTags into ErrorTags and Error List items
/// </summary>
internal sealed class ErrorTagger : ITagger<IErrorTag>
{
ITextBuffer _buffer;
ITagAggregator<IDafnyResolverTag> _aggregator;
internal ErrorTagger(ITextBuffer buffer, ITagAggregator<IDafnyResolverTag> tagAggregator) {
_buffer = buffer;
_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<IErrorTag>> GetTags(NormalizedSnapshotSpanCollection spans) {
if (spans.Count == 0) yield break;
var snapshot = spans[0].Snapshot;
foreach (var tagSpan in _aggregator.GetTags(spans)) {
var et = tagSpan.Tag as IErrorTag;
if (et != null) {
foreach (SnapshotSpan s in tagSpan.Span.GetSpans(snapshot)) {
yield return new TagSpan<IErrorTag>(s, et);
}
}
}
}
// 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 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));
}
}
}
}
#endregion
}
|
