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
|
using System;
using System.Collections.Generic;
using System.ComponentModel.Composition;
using System.Windows.Media;
using Microsoft.VisualStudio.Text;
using Microsoft.VisualStudio.Text.Classification;
using Microsoft.VisualStudio.Text.Editor;
using Microsoft.VisualStudio.Text.Tagging;
using Microsoft.VisualStudio.Utilities;
namespace DafnyLanguage
{
[Export(typeof(ITaggerProvider))]
[ContentType("dafny")]
[TagType(typeof(ClassificationTag))]
internal sealed class DafnyClassifierProvider : ITaggerProvider
{
[Import]
internal IBufferTagAggregatorFactoryService AggregatorFactory = null;
[Import]
internal IClassificationTypeRegistryService ClassificationTypeRegistry = null;
[Import]
internal Microsoft.VisualStudio.Language.StandardClassification.IStandardClassificationService Standards = null;
public ITagger<T> CreateTagger<T>(ITextBuffer buffer) where T : ITag {
ITagAggregator<DafnyTokenTag> tagAggregator = AggregatorFactory.CreateTagAggregator<DafnyTokenTag>(buffer);
return new DafnyClassifier(buffer, tagAggregator, ClassificationTypeRegistry, Standards) as ITagger<T>;
}
}
internal sealed class DafnyClassifier : ITagger<ClassificationTag>
{
ITextBuffer _buffer;
ITagAggregator<DafnyTokenTag> _aggregator;
IDictionary<DafnyTokenKinds, IClassificationType> _typeMap;
internal DafnyClassifier(ITextBuffer buffer,
ITagAggregator<DafnyTokenTag> tagAggregator,
IClassificationTypeRegistryService typeService, Microsoft.VisualStudio.Language.StandardClassification.IStandardClassificationService standards) {
_buffer = buffer;
_aggregator = tagAggregator;
_aggregator.TagsChanged += new EventHandler<TagsChangedEventArgs>(_aggregator_TagsChanged);
// use built-in classification types:
_typeMap = new Dictionary<DafnyTokenKinds, IClassificationType>();
_typeMap[DafnyTokenKinds.Keyword] = standards.Keyword;
_typeMap[DafnyTokenKinds.Number] = standards.NumberLiteral;
_typeMap[DafnyTokenKinds.String] = standards.StringLiteral;
_typeMap[DafnyTokenKinds.Comment] = standards.Comment;
_typeMap[DafnyTokenKinds.VariableIdentifier] = standards.Identifier;
_typeMap[DafnyTokenKinds.VariableIdentifierDefinition] = typeService.GetClassificationType("Dafny identifier");
}
public event EventHandler<SnapshotSpanEventArgs> TagsChanged;
public IEnumerable<ITagSpan<ClassificationTag>> GetTags(NormalizedSnapshotSpanCollection spans) {
if (spans.Count == 0) yield break;
var snapshot = spans[0].Snapshot;
foreach (var tagSpan in this._aggregator.GetTags(spans)) {
IClassificationType t = _typeMap[tagSpan.Tag.Kind];
foreach (SnapshotSpan s in tagSpan.Span.GetSpans(snapshot)) {
yield return new TagSpan<ClassificationTag>(s, new ClassificationTag(t));
}
}
}
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));
}
}
}
}
/// <summary>
/// Defines an editor format for user-defined type.
/// </summary>
[Export(typeof(EditorFormatDefinition))]
[ClassificationType(ClassificationTypeNames = "Dafny identifier")]
[Name("Dafny identifier")]
[UserVisible(true)]
//set the priority to be after the default classifiers
[Order(Before = Priority.Default)]
internal sealed class DafnyTypeFormat : ClassificationFormatDefinition
{
public DafnyTypeFormat() {
this.DisplayName = "Dafny identifier"; //human readable version of the name
this.ForegroundColor = Colors.CornflowerBlue;
}
}
internal static class ClassificationDefinition
{
/// <summary>
/// Defines the "ordinary" classification type.
/// </summary>
[Export(typeof(ClassificationTypeDefinition))]
[Name("Dafny identifier")]
internal static ClassificationTypeDefinition UserType = null;
}
}
|
