blob: a4f232dd9e39856555648981610aa550a96bf372 (
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
91
92
93
94
95
96
97
98
|
using System;
using System.Collections.Generic;
using System.Windows;
using System.Windows.Shapes;
using System.Windows.Media;
using System.Windows.Controls;
using System.ComponentModel.Composition;
using Microsoft.VisualStudio.Text;
using Microsoft.VisualStudio.Text.Editor;
using Microsoft.VisualStudio.Text.Formatting;
using Microsoft.VisualStudio.Text.Tagging;
using Microsoft.VisualStudio.Text.Classification;
using Microsoft.VisualStudio.Utilities;
using System.Diagnostics.Contracts;
namespace DafnyLanguage
{
internal class ProgressMarginGlyphFactory : IGlyphFactory
{
const double m_glyphSize = 16.0;
public UIElement GenerateGlyph(IWpfTextViewLine line, IGlyphTag tag) {
var dtag = tag as ProgressGlyphTag;
if (dtag == null) {
return null;
}
System.Windows.Shapes.Ellipse ellipse = new Ellipse();
ellipse.Fill = Brushes.LightBlue;
ellipse.StrokeThickness = 2;
ellipse.Stroke = dtag.V == 0 ? Brushes.DarkBlue : Brushes.BlanchedAlmond;
ellipse.Height = m_glyphSize;
ellipse.Width = m_glyphSize;
return ellipse;
}
}
[Export(typeof(IGlyphFactoryProvider))]
[Name("ProgressMarginGlyph")]
[Order(After = "TokenTagger")]
[ContentType("dafny")]
[TagType(typeof(ProgressGlyphTag))]
internal sealed class ProgressMarginGlyphFactoryProvider : IGlyphFactoryProvider
{
public IGlyphFactory GetGlyphFactory(IWpfTextView view, IWpfTextViewMargin margin) {
return new ProgressMarginGlyphFactory();
}
}
internal class ProgressGlyphTag : IGlyphTag
{
public int V;
public ProgressGlyphTag(int v) {
V = v;
}
}
internal class ProgressTagger : ITagger<ProgressGlyphTag>
{
public ProgressTagger(ITextBuffer buffer) {
BufferIdleEventUtil.AddBufferIdleEventListener(buffer, ClearMarks);
}
ITextVersion latestClearedVersion;
public void ClearMarks(object sender, EventArgs args) {
var buffer = sender as ITextBuffer;
var chng = TagsChanged;
if (buffer != null && chng != null) {
var snap = buffer.CurrentSnapshot;
latestClearedVersion = snap.Version;
chng(this, new SnapshotSpanEventArgs(new SnapshotSpan(snap, 0, snap.Length)));
}
}
IEnumerable<ITagSpan<ProgressGlyphTag>> ITagger<ProgressGlyphTag>.GetTags(NormalizedSnapshotSpanCollection spans) {
if (spans.Count == 0) yield break;
if (spans[0].Snapshot.Version != latestClearedVersion) {
foreach (SnapshotSpan span in spans) {
yield return new TagSpan<ProgressGlyphTag>(new SnapshotSpan(span.Start, span.Length), new ProgressGlyphTag(1));
}
}
}
public event EventHandler<SnapshotSpanEventArgs> TagsChanged;
}
[Export(typeof(ITaggerProvider))]
[ContentType("dafny")]
[TagType(typeof(ProgressGlyphTag))]
class ProgressTaggerProvider : ITaggerProvider
{
public ITagger<T> CreateTagger<T>(ITextBuffer buffer) where T : ITag {
return new ProgressTagger(buffer) as ITagger<T>;
}
}
}
|
