diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-10-04 13:32:50 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-10-04 13:32:50 -0700 |
| commit | 8911e5c95d4715c2e2626aef67f19793d6f43201 (patch) | |
| tree | d703bfd931802e780430e32f1339cf77adc342a4 /Source/DafnyExtension/ErrorTagger.cs | |
| parent | 1c375d1889e628fcd2a1a0fc041673a5f4230d84 (diff) | |
Put all sources under \Source directory
Diffstat (limited to 'Source/DafnyExtension/ErrorTagger.cs')
| -rw-r--r-- | Source/DafnyExtension/ErrorTagger.cs | 85 |
1 files changed, 85 insertions, 0 deletions
diff --git a/Source/DafnyExtension/ErrorTagger.cs b/Source/DafnyExtension/ErrorTagger.cs new file mode 100644 index 00000000..efd755d8 --- /dev/null +++ b/Source/DafnyExtension/ErrorTagger.cs @@ -0,0 +1,85 @@ +//***************************************************************************
+// 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 EnvDTE;
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.ComponentModel.Composition;
+using System.Windows.Threading;
+using Microsoft.VisualStudio.Shell;
+using Microsoft.VisualStudio.Shell.Interop;
+using Microsoft.VisualStudio.Text;
+using Microsoft.VisualStudio.Text.Classification;
+using Microsoft.VisualStudio.Text.Editor;
+using Microsoft.VisualStudio.Text.Tagging;
+using Microsoft.VisualStudio.Text.Projection;
+using Microsoft.VisualStudio.Utilities;
+
+namespace DafnyLanguage
+{
+ [Export(typeof(ITaggerProvider))]
+ [ContentType("dafny")]
+ [TagType(typeof(ErrorTag))]
+ internal sealed class ErrorTaggerProvider : ITaggerProvider
+ {
+ [Import]
+ internal IBufferTagAggregatorFactoryService AggregatorFactory = null;
+
+ public ITagger<T> CreateTagger<T>(ITextBuffer buffer) where T : ITag {
+ ITagAggregator<DafnyResolverTag> tagAggregator = AggregatorFactory.CreateTagAggregator<DafnyResolverTag>(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);
+ }
+ }
+
+ /// <summary>
+ /// Translate PkgDefTokenTags into ErrorTags and Error List items
+ /// </summary>
+ internal sealed class ErrorTagger : ITagger<ErrorTag>
+ {
+ ITextBuffer _buffer;
+ ITagAggregator<DafnyResolverTag> _aggregator;
+
+ internal ErrorTagger(ITextBuffer buffer, ITagAggregator<DafnyResolverTag> 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<ErrorTag>> GetTags(NormalizedSnapshotSpanCollection spans) {
+ if (spans.Count == 0) yield break;
+ var snapshot = spans[0].Snapshot;
+ foreach (var tagSpan in this._aggregator.GetTags(spans)) {
+ DafnyResolverTag t = tagSpan.Tag;
+ DafnyErrorResolverTag et = t as DafnyErrorResolverTag;
+ if (et != null) {
+ foreach (SnapshotSpan s in tagSpan.Span.GetSpans(snapshot)) {
+ yield return new TagSpan<ErrorTag>(s, new ErrorTag(et.Typ, et.Msg));
+ }
+ }
+ }
+ }
+
+ // 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));
+ }
+ }
+ }
+ }
+}
|