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
|
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Windows.Input;
using Microsoft.VisualStudio.Language.Intellisense;
using System.Collections.ObjectModel;
using Microsoft.VisualStudio.Text;
using Microsoft.VisualStudio.Text.Editor;
using Microsoft.VisualStudio.Text.Tagging;
using System.ComponentModel.Composition;
using Microsoft.VisualStudio.Utilities;
using System.Diagnostics.Contracts;
namespace DafnyLanguage
{
[Export(typeof(IQuickInfoSourceProvider))]
[ContentType("dafny")]
[Name("Dafny QuickInfo")]
class OokQuickInfoSourceProvider : IQuickInfoSourceProvider
{
[Import]
IBufferTagAggregatorFactoryService aggService = null;
public IQuickInfoSource TryCreateQuickInfoSource(ITextBuffer textBuffer) {
return new OokQuickInfoSource(textBuffer, aggService.CreateTagAggregator<DafnyTokenTag>(textBuffer));
}
}
class OokQuickInfoSource : IQuickInfoSource
{
private ITagAggregator<DafnyTokenTag> _aggregator;
private ITextBuffer _buffer;
private bool _disposed = false;
public OokQuickInfoSource(ITextBuffer buffer, ITagAggregator<DafnyTokenTag> aggregator) {
_aggregator = aggregator;
_buffer = buffer;
}
public void AugmentQuickInfoSession(IQuickInfoSession session, IList<object> quickInfoContent, out ITrackingSpan applicableToSpan) {
applicableToSpan = null;
if (_disposed)
throw new ObjectDisposedException("TestQuickInfoSource");
var triggerPoint = (SnapshotPoint)session.GetTriggerPoint(_buffer.CurrentSnapshot);
if (triggerPoint == null)
return;
foreach (IMappingTagSpan<DafnyTokenTag> curTag in _aggregator.GetTags(new SnapshotSpan(triggerPoint, triggerPoint))) {
var s = curTag.Tag.HoverText;
if (s != null) {
var tagSpan = curTag.Span.GetSpans(_buffer).First();
applicableToSpan = _buffer.CurrentSnapshot.CreateTrackingSpan(tagSpan, SpanTrackingMode.EdgeExclusive);
quickInfoContent.Add(s);
}
}
}
public void Dispose() {
_disposed = true;
}
}
// --------------------------------- QuickInfo controller ------------------------------------------
[Export(typeof(IIntellisenseControllerProvider))]
[Name("Dafny QuickInfo controller")]
[ContentType("dafny")]
class DafnyQuickInfoControllerProvider : IIntellisenseControllerProvider
{
[Import]
internal IQuickInfoBroker QuickInfoBroker { get; set; }
public IIntellisenseController TryCreateIntellisenseController(ITextView textView, IList<ITextBuffer> subjectBuffers) {
return new DafnyQuickInfoController(textView, subjectBuffers, this);
}
}
class DafnyQuickInfoController : IIntellisenseController
{
private ITextView _textView;
private IList<ITextBuffer> _subjectBuffers;
private DafnyQuickInfoControllerProvider _componentContext;
private IQuickInfoSession _session;
internal DafnyQuickInfoController(ITextView textView, IList<ITextBuffer> subjectBuffers, DafnyQuickInfoControllerProvider componentContext) {
_textView = textView;
_subjectBuffers = subjectBuffers;
_componentContext = componentContext;
_textView.MouseHover += this.OnTextViewMouseHover;
}
public void ConnectSubjectBuffer(ITextBuffer subjectBuffer) {
}
public void DisconnectSubjectBuffer(ITextBuffer subjectBuffer) {
}
public void Detach(ITextView textView) {
if (_textView == textView) {
_textView.MouseHover -= OnTextViewMouseHover;
_textView = null;
}
}
void OnTextViewMouseHover(object sender, MouseHoverEventArgs e) {
SnapshotPoint? point = GetMousePosition(new SnapshotPoint(_textView.TextSnapshot, e.Position));
if (point != null) {
ITrackingPoint triggerPoint = point.Value.Snapshot.CreateTrackingPoint(point.Value.Position, PointTrackingMode.Positive);
// Find the broker for this buffer
if (!_componentContext.QuickInfoBroker.IsQuickInfoActive(_textView)) {
_session = _componentContext.QuickInfoBroker.CreateQuickInfoSession(_textView, triggerPoint, true);
_session.Start();
}
}
}
SnapshotPoint? GetMousePosition(SnapshotPoint topPosition) {
return _textView.BufferGraph.MapDownToFirstMatch(
topPosition,
PointTrackingMode.Positive,
snapshot => _subjectBuffers.Contains(snapshot.TextBuffer),
PositionAffinity.Predecessor);
}
}
}
|
