diff options
| author |  wuestholz <unknown> | 2013-07-15 18:54:34 -0700 |
|---|---|---|
| committer | wuestholz <unknown> | 2013-07-15 18:54:34 -0700 |
| commit | 832510796b7feb7f48cad8011aa688b2639668fa (patch) | |
| tree | 14f3800d3b5d972fce96f01185f5710167c3041e | |
| parent | 8b69f963879696d40da0a1b845988e17fe9d29d2 (diff) | |
DafnyExtension: Added support for selecting errors and showing the model in BVD.
| -rw-r--r-- | Source/DafnyExtension/ContentType.cs | 16 | ||||
| -rw-r--r-- | Source/DafnyExtension/DafnyExtension.csproj | 2 | ||||
| -rw-r--r-- | Source/DafnyExtension/ErrorModelTagger.cs | 179 | ||||
| -rw-r--r-- | Source/DafnyExtension/ErrorTagger.cs | 18 | ||||
| -rw-r--r-- | Source/DafnyExtension/IdentifierTagger.cs | 6 | ||||
| -rw-r--r-- | Source/DafnyExtension/IntraTextAdornmentTagger.cs | 252 | ||||
| -rw-r--r-- | Source/DafnyExtension/OutliningTagger.cs | 6 | ||||
| -rw-r--r-- | Source/DafnyExtension/ProgressMargin.cs | 19 | ||||
| -rw-r--r-- | Source/DafnyExtension/ResolverTagger.cs | 84 | ||||
| -rw-r--r-- | Source/DafnyMenu/DafnyMenu.vsct | 2 | ||||
| -rw-r--r-- | Source/DafnyMenu/DafnyMenuPackage.cs | 11 |
11 files changed, 534 insertions, 61 deletions
diff --git a/Source/DafnyExtension/ContentType.cs b/Source/DafnyExtension/ContentType.cs index 950b1e73..c528f4ed 100644 --- a/Source/DafnyExtension/ContentType.cs +++ b/Source/DafnyExtension/ContentType.cs @@ -1,4 +1,5 @@ using System.ComponentModel.Composition;
+using Microsoft.VisualStudio.Text.Editor;
using Microsoft.VisualStudio.Utilities;
@@ -11,6 +12,21 @@ namespace DafnyLanguage [BaseDefinition("code")]
internal static ContentTypeDefinition ContentType = null;
+ [Export(typeof(IWpfTextViewCreationListener))]
+ [ContentType("text")]
+ [TextViewRole(PredefinedTextViewRoles.Document)]
+ internal sealed class DafnyTextViewCreationListener : IWpfTextViewCreationListener
+ {
+ [Export(typeof(AdornmentLayerDefinition))]
+ [Name("ModelAdornment")]
+ [Order(After = PredefinedAdornmentLayers.Selection, Before = PredefinedAdornmentLayers.Text)]
+ [TextViewRole(PredefinedTextViewRoles.Document)]
+ public AdornmentLayerDefinition editorAdornmentLayer = null;
+ public void TextViewCreated(IWpfTextView textView)
+ {
+ }
+ }
+
[Export]
[FileExtension(".dfy")]
[ContentType("dafny")]
diff --git a/Source/DafnyExtension/DafnyExtension.csproj b/Source/DafnyExtension/DafnyExtension.csproj index d76de86d..e5a679fd 100644 --- a/Source/DafnyExtension/DafnyExtension.csproj +++ b/Source/DafnyExtension/DafnyExtension.csproj @@ -187,9 +187,11 @@ </ItemGroup>
<ItemGroup>
<Compile Include="BufferIdleEventUtil.cs" />
+ <Compile Include="ErrorModelTagger.cs" />
<Compile Include="GlobalSuppressions.cs" />
<Compile Include="HoverText.cs" />
<Compile Include="IdentifierTagger.cs" />
+ <Compile Include="IntraTextAdornmentTagger.cs" />
<Compile Include="ProgressMargin.cs" />
<Compile Include="OutliningTagger.cs" />
<Compile Include="ResolverTagger.cs" />
diff --git a/Source/DafnyExtension/ErrorModelTagger.cs b/Source/DafnyExtension/ErrorModelTagger.cs new file mode 100644 index 00000000..15e1c2ea --- /dev/null +++ b/Source/DafnyExtension/ErrorModelTagger.cs @@ -0,0 +1,179 @@ +//***************************************************************************
+// 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 System.Diagnostics.Contracts;
+using System.Windows;
+using System.Windows.Input;
+using System.Windows.Media;
+using System.Windows.Shapes;
+using Microsoft.VisualStudio.Text;
+using Microsoft.VisualStudio.Text.Editor;
+using Microsoft.VisualStudio.Text.Tagging;
+using Microsoft.VisualStudio.Utilities;
+
+
+namespace DafnyLanguage
+{
+
+ #region Provider
+
+ [Export(typeof(IViewTaggerProvider))]
+ [ContentType("dafny")]
+ [Name("ErrorModelTagger")]
+ [Order(After = "ErrorTagger")]
+ [TextViewRole(PredefinedTextViewRoles.Document)]
+ [TagType(typeof(IntraTextAdornmentTag))]
+ internal sealed class ErrorModelTaggerProvider : IViewTaggerProvider
+ {
+ [Import]
+ internal IBufferTagAggregatorFactoryService BufferTagAggregatorFactoryService = null;
+
+ public ITagger<T> CreateTagger<T>(ITextView textView, ITextBuffer buffer) where T : ITag
+ {
+ if (textView == null)
+ throw new ArgumentNullException("textView");
+
+ if (buffer == null)
+ throw new ArgumentNullException("buffer");
+
+ if (buffer != textView.TextBuffer)
+ return null;
+
+ return ErrorModelTagger.GetTagger(
+ (IWpfTextView)textView,
+ new Lazy<ITagAggregator<IDafnyResolverTag>>(
+ () => BufferTagAggregatorFactoryService.CreateTagAggregator<IDafnyResolverTag>(textView.TextBuffer)))
+ as ITagger<T>;
+ }
+ }
+
+ #endregion
+
+
+ #region Tagger
+
+ internal sealed class ErrorModelTagger : IntraTextAdornmentTagger<IDafnyResolverTag, Ellipse>, IDisposable
+ {
+ IWpfTextView _view;
+ ITagAggregator<IDafnyResolverTag> _aggregator;
+
+ internal static ITagger<IntraTextAdornmentTag> GetTagger(IWpfTextView view, Lazy<ITagAggregator<IDafnyResolverTag>> aggregator)
+ {
+ return view.Properties.GetOrCreateSingletonProperty<ErrorModelTagger>(
+ () => new ErrorModelTagger(view, aggregator.Value));
+ }
+
+ private ErrorModelTagger(IWpfTextView view, ITagAggregator<IDafnyResolverTag> aggregator)
+ : base(view)
+ {
+ _view = view;
+ _aggregator = aggregator;
+ _aggregator.TagsChanged += new EventHandler<TagsChangedEventArgs>(_aggregator_TagsChanged);
+ }
+
+ public void Dispose()
+ {
+ this._aggregator.Dispose();
+
+ base.view.Properties.RemoveProperty(typeof(ErrorModelTagger));
+ }
+
+ // To produce adornments that don't obscure the text, the adornment tags
+ // should have zero length spans. Overriding this method allows control
+ // over the tag spans.
+ protected override IEnumerable<Tuple<SnapshotSpan, PositionAffinity?, IDafnyResolverTag>> GetAdornmentData(NormalizedSnapshotSpanCollection spans)
+ {
+ if (spans.Count == 0)
+ yield break;
+
+ ITextSnapshot snapshot = spans[0].Snapshot;
+
+ var tags = this._aggregator.GetTags(spans);
+
+ foreach (IMappingTagSpan<IDafnyResolverTag> tag in tags)
+ {
+ var ertag = tag.Tag as DafnyErrorResolverTag;
+ if (ertag != null && ertag.Error.Model != null)
+ {
+ NormalizedSnapshotSpanCollection normSpans = tag.Span.GetSpans(snapshot);
+
+ // Ignore data tags that are split by projection.
+ // This is theoretically possible but unlikely in current scenarios.
+ if (normSpans.Count != 1)
+ continue;
+
+ yield return Tuple.Create(new SnapshotSpan(normSpans[0].Start, 0), (PositionAffinity?)PositionAffinity.Successor, tag.Tag);
+ }
+ }
+ }
+
+ protected override Ellipse CreateAdornment(IDafnyResolverTag data, SnapshotSpan span)
+ {
+ var ertag = data as DafnyErrorResolverTag;
+ Contract.Assert(ertag != null);
+
+ var result = new Ellipse
+ {
+ Fill = Brushes.Red,
+ Height = 12.0, Width = 12.0,
+ ToolTip = "select error",
+ StrokeThickness = 3.0,
+ Stroke = Brushes.Red,
+ Cursor = Cursors.Arrow,
+
+ };
+ result.MouseDown += new MouseButtonEventHandler((s, e) =>
+ {
+ if (ertag.Error.SelectedError == ertag.Error)
+ {
+ // unselect it
+ ertag.Error.SelectedError = null;
+ result.Stroke = Brushes.Red;
+ result.ToolTip = "select error";
+ }
+ else
+ {
+ // unselect the old one
+ if (ertag.Error.SelectedError != null)
+ {
+ ertag.Error.SelectedError.Adornment.Stroke = Brushes.Red;
+ ertag.Error.SelectedError.Adornment.ToolTip = "select error";
+ ertag.Error.SelectedError = null;
+ }
+
+ // select the new one
+ ertag.Error.SelectedError = ertag.Error;
+ ertag.Error.Adornment = result;
+ ertag.Error.Adornment.Stroke = Brushes.Black;
+ ertag.Error.Adornment.ToolTip = "unselect error";
+ }
+ });
+ return result;
+ }
+
+ protected override bool UpdateAdornment(Ellipse adornment, IDafnyResolverTag data)
+ {
+ return false;
+ }
+
+ void _aggregator_TagsChanged(object sender, TagsChangedEventArgs e)
+ {
+ NormalizedSnapshotSpanCollection spans = e.Span.GetSpans(_view.TextBuffer.CurrentSnapshot);
+ if (spans.Count > 0)
+ {
+ var span = new SnapshotSpan(spans[0].Start, spans[spans.Count - 1].End);
+ InvalidateSpans(new List<SnapshotSpan> { span });
+ }
+ }
+ }
+
+ #endregion
+
+}
diff --git a/Source/DafnyExtension/ErrorTagger.cs b/Source/DafnyExtension/ErrorTagger.cs index 74765203..2b8a4708 100644 --- a/Source/DafnyExtension/ErrorTagger.cs +++ b/Source/DafnyExtension/ErrorTagger.cs @@ -19,15 +19,16 @@ namespace DafnyLanguage #region Provider
[Export(typeof(ITaggerProvider))]
+ [Name("ErrorTagger")]
[ContentType("dafny")]
- [TagType(typeof(ErrorTag))]
+ [TagType(typeof(IErrorTag))]
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);
+ 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);
@@ -42,12 +43,12 @@ namespace DafnyLanguage /// <summary>
/// Translate PkgDefTokenTags into ErrorTags and Error List items
/// </summary>
- internal sealed class ErrorTagger : ITagger<ErrorTag>
+ internal sealed class ErrorTagger : ITagger<IErrorTag>
{
ITextBuffer _buffer;
- ITagAggregator<DafnyResolverTag> _aggregator;
+ ITagAggregator<IDafnyResolverTag> _aggregator;
- internal ErrorTagger(ITextBuffer buffer, ITagAggregator<DafnyResolverTag> tagAggregator) {
+ internal ErrorTagger(ITextBuffer buffer, ITagAggregator<IDafnyResolverTag> tagAggregator) {
_buffer = buffer;
_aggregator = tagAggregator;
_aggregator.TagsChanged += new EventHandler<TagsChangedEventArgs>(_aggregator_TagsChanged);
@@ -56,15 +57,14 @@ namespace DafnyLanguage /// <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) {
+ public IEnumerable<ITagSpan<IErrorTag>> 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;
+ var et = tagSpan.Tag as IErrorTag;
if (et != null) {
foreach (SnapshotSpan s in tagSpan.Span.GetSpans(snapshot)) {
- yield return new TagSpan<ErrorTag>(s, new ErrorTag(et.Typ, et.Msg));
+ yield return new TagSpan<IErrorTag>(s, et);
}
}
}
diff --git a/Source/DafnyExtension/IdentifierTagger.cs b/Source/DafnyExtension/IdentifierTagger.cs index e334271f..837d48ed 100644 --- a/Source/DafnyExtension/IdentifierTagger.cs +++ b/Source/DafnyExtension/IdentifierTagger.cs @@ -30,7 +30,7 @@ namespace DafnyLanguage internal IBufferTagAggregatorFactoryService AggregatorFactory = null;
public ITagger<T> CreateTagger<T>(ITextBuffer buffer) where T : ITag {
- ITagAggregator<DafnyResolverTag> tagAggregator = AggregatorFactory.CreateTagAggregator<DafnyResolverTag>(buffer);
+ ITagAggregator<IDafnyResolverTag> tagAggregator = AggregatorFactory.CreateTagAggregator<IDafnyResolverTag>(buffer);
// create a single tagger for each buffer.
Func<ITagger<T>> sc = delegate() { return new IdentifierTagger(buffer, tagAggregator) as ITagger<T>; };
return buffer.Properties.GetOrCreateSingletonProperty<ITagger<T>>(sc);
@@ -51,9 +51,9 @@ namespace DafnyLanguage ITextSnapshot _snapshot; // the most recent snapshot of _buffer that we have been informed about
Microsoft.Dafny.Program _program; // the program parsed from _snapshot
List<IdRegion> _regions = new List<IdRegion>(); // the regions generated from _program
- ITagAggregator<DafnyResolverTag> _aggregator;
+ ITagAggregator<IDafnyResolverTag> _aggregator;
- internal IdentifierTagger(ITextBuffer buffer, ITagAggregator<DafnyResolverTag> tagAggregator) {
+ internal IdentifierTagger(ITextBuffer buffer, ITagAggregator<IDafnyResolverTag> tagAggregator) {
_buffer = buffer;
_snapshot = _buffer.CurrentSnapshot;
_aggregator = tagAggregator;
diff --git a/Source/DafnyExtension/IntraTextAdornmentTagger.cs b/Source/DafnyExtension/IntraTextAdornmentTagger.cs new file mode 100644 index 00000000..8d789d2f --- /dev/null +++ b/Source/DafnyExtension/IntraTextAdornmentTagger.cs @@ -0,0 +1,252 @@ +//***************************************************************************
+//
+// Copyright (c) Microsoft Corporation. All rights reserved.
+// This code is licensed under the Visual Studio SDK license terms.
+// THIS CODE IS PROVIDED *AS IS* WITHOUT WARRANTY OF
+// ANY KIND, EITHER EXPRESS OR IMPLIED, INCLUDING ANY
+// IMPLIED WARRANTIES OF FITNESS FOR A PARTICULAR
+// PURPOSE, MERCHANTABILITY, OR NON-INFRINGEMENT.
+//
+//***************************************************************************
+
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Windows;
+using Microsoft.VisualStudio.Text;
+using Microsoft.VisualStudio.Text.Editor;
+using Microsoft.VisualStudio.Text.Tagging;
+
+namespace DafnyLanguage
+{
+ /// <summary>
+ /// Helper class for interspersing adornments into text.
+ /// </summary>
+ /// <remarks>
+ /// To avoid an issue around intra-text adornment support and its interaction with text buffer changes,
+ /// this tagger reacts to text and color tag changes with a delay. It waits to send out its own TagsChanged
+ /// event until the WPF Dispatcher is running again and it takes care to report adornments
+ /// that are consistent with the latest sent TagsChanged event by storing that particular snapshot
+ /// and using it to query for the data tags.
+ /// </remarks>
+ internal abstract class IntraTextAdornmentTagger<TData, TAdornment>
+ : ITagger<IntraTextAdornmentTag>
+ where TAdornment : UIElement
+ {
+ protected readonly IWpfTextView view;
+ private Dictionary<SnapshotSpan, TAdornment> adornmentCache = new Dictionary<SnapshotSpan, TAdornment>();
+ protected ITextSnapshot snapshot { get; private set; }
+ private readonly List<SnapshotSpan> invalidatedSpans = new List<SnapshotSpan>();
+
+ protected IntraTextAdornmentTagger(IWpfTextView view)
+ {
+ this.view = view;
+ this.snapshot = view.TextBuffer.CurrentSnapshot;
+
+ this.view.LayoutChanged += HandleLayoutChanged;
+ this.view.TextBuffer.Changed += HandleBufferChanged;
+ }
+
+ /// <param name="span">The span of text that this adornment will elide.</param>
+ /// <returns>Adornment corresponding to given data. May be null.</returns>
+ protected abstract TAdornment CreateAdornment(TData data, SnapshotSpan span);
+
+ /// <returns>True if the adornment was updated and should be kept. False to have the adornment removed from the view.</returns>
+ protected abstract bool UpdateAdornment(TAdornment adornment, TData data);
+
+ /// <param name="spans">Spans to provide adornment data for. These spans do not necessarily correspond to text lines.</param>
+ /// <remarks>
+ /// If adornments need to be updated, call <see cref="RaiseTagsChanged"/> or <see cref="InavlidateSpans"/>.
+ /// This will, indirectly, cause <see cref="GetAdornmentData"/> to be called.
+ /// </remarks>
+ /// <returns>
+ /// A sequence of:
+ /// * adornment data for each adornment to be displayed
+ /// * the span of text that should be elided for that adornment (zero length spans are acceptable)
+ /// * and affinity of the adornment (this should be null if and only if the elided span has a length greater than zero)
+ /// </returns>
+ protected abstract IEnumerable<Tuple<SnapshotSpan, PositionAffinity?, TData>> GetAdornmentData(NormalizedSnapshotSpanCollection spans);
+
+ private void HandleBufferChanged(object sender, TextContentChangedEventArgs args)
+ {
+ var editedSpans = args.Changes.Select(change => new SnapshotSpan(args.After, change.NewSpan)).ToList();
+ InvalidateSpans(editedSpans);
+ }
+
+ /// <summary>
+ /// Causes intra-text adornments to be updated asynchronously.
+ /// </summary>
+ protected void InvalidateSpans(IList<SnapshotSpan> spans)
+ {
+ lock (this.invalidatedSpans)
+ {
+ bool wasEmpty = this.invalidatedSpans.Count == 0;
+ this.invalidatedSpans.AddRange(spans);
+
+ if (wasEmpty && this.invalidatedSpans.Count > 0)
+ this.view.VisualElement.Dispatcher.BeginInvoke(new Action(AsyncUpdate));
+ }
+ }
+
+ private void AsyncUpdate()
+ {
+ // Store the snapshot that we're now current with and send an event
+ // for the text that has changed.
+ if (this.snapshot != this.view.TextBuffer.CurrentSnapshot)
+ {
+ this.snapshot = this.view.TextBuffer.CurrentSnapshot;
+
+ Dictionary<SnapshotSpan, TAdornment> translatedAdornmentCache = new Dictionary<SnapshotSpan, TAdornment>();
+
+ foreach (var keyValuePair in this.adornmentCache)
+ translatedAdornmentCache.Add(keyValuePair.Key.TranslateTo(this.snapshot, SpanTrackingMode.EdgeExclusive), keyValuePair.Value);
+
+ this.adornmentCache = translatedAdornmentCache;
+ }
+
+ List<SnapshotSpan> translatedSpans;
+ lock (this.invalidatedSpans)
+ {
+ translatedSpans = this.invalidatedSpans.Select(s => s.TranslateTo(this.snapshot, SpanTrackingMode.EdgeInclusive)).ToList();
+ this.invalidatedSpans.Clear();
+ }
+
+ if (translatedSpans.Count == 0)
+ return;
+
+ var start = translatedSpans.Select(span => span.Start).Min();
+ var end = translatedSpans.Select(span => span.End).Max();
+
+ RaiseTagsChanged(new SnapshotSpan(start, end));
+ }
+
+ /// <summary>
+ /// Causes intra-text adornments to be updated synchronously.
+ /// </summary>
+ protected void RaiseTagsChanged(SnapshotSpan span)
+ {
+ var handler = this.TagsChanged;
+ if (handler != null)
+ handler(this, new SnapshotSpanEventArgs(span));
+ }
+
+ private void HandleLayoutChanged(object sender, TextViewLayoutChangedEventArgs e)
+ {
+ SnapshotSpan visibleSpan = this.view.TextViewLines.FormattedSpan;
+
+ // Filter out the adornments that are no longer visible.
+ List<SnapshotSpan> toRemove = new List<SnapshotSpan>(
+ from keyValuePair
+ in this.adornmentCache
+ where !keyValuePair.Key.TranslateTo(visibleSpan.Snapshot, SpanTrackingMode.EdgeExclusive).IntersectsWith(visibleSpan)
+ select keyValuePair.Key);
+
+ foreach (var span in toRemove)
+ this.adornmentCache.Remove(span);
+ }
+
+
+ // Produces tags on the snapshot that the tag consumer asked for.
+ public virtual IEnumerable<ITagSpan<IntraTextAdornmentTag>> GetTags(NormalizedSnapshotSpanCollection spans)
+ {
+ if (spans == null || spans.Count == 0)
+ yield break;
+
+ // Translate the request to the snapshot that this tagger is current with.
+
+ ITextSnapshot requestedSnapshot = spans[0].Snapshot;
+
+ var translatedSpans = new NormalizedSnapshotSpanCollection(spans.Select(span => span.TranslateTo(this.snapshot, SpanTrackingMode.EdgeExclusive)));
+
+ // Grab the adornments.
+ foreach (var tagSpan in GetAdornmentTagsOnSnapshot(translatedSpans))
+ {
+ // Translate each adornment to the snapshot that the tagger was asked about.
+ SnapshotSpan span = tagSpan.Span.TranslateTo(requestedSnapshot, SpanTrackingMode.EdgeExclusive);
+
+ IntraTextAdornmentTag tag = new IntraTextAdornmentTag(tagSpan.Tag.Adornment, tagSpan.Tag.RemovalCallback, tagSpan.Tag.Affinity);
+ yield return new TagSpan<IntraTextAdornmentTag>(span, tag);
+ }
+ }
+
+ // Produces tags on the snapshot that this tagger is current with.
+ private IEnumerable<TagSpan<IntraTextAdornmentTag>> GetAdornmentTagsOnSnapshot(NormalizedSnapshotSpanCollection spans)
+ {
+ if (spans.Count == 0)
+ yield break;
+
+ ITextSnapshot snapshot = spans[0].Snapshot;
+
+ System.Diagnostics.Debug.Assert(snapshot == this.snapshot);
+
+ // Since WPF UI objects have state (like mouse hover or animation) and are relatively expensive to create and lay out,
+ // this code tries to reuse controls as much as possible.
+ // The controls are stored in this.adornmentCache between the calls.
+
+ // Mark which adornments fall inside the requested spans with Keep=false
+ // so that they can be removed from the cache if they no longer correspond to data tags.
+ HashSet<SnapshotSpan> toRemove = new HashSet<SnapshotSpan>();
+ foreach (var ar in this.adornmentCache)
+ if (spans.IntersectsWith(new NormalizedSnapshotSpanCollection(ar.Key)))
+ toRemove.Add(ar.Key);
+
+ foreach (var spanDataPair in GetAdornmentData(spans).Distinct(new Comparer()))
+ {
+ // Look up the corresponding adornment or create one if it's new.
+ TAdornment adornment;
+ SnapshotSpan snapshotSpan = spanDataPair.Item1;
+ PositionAffinity? affinity = spanDataPair.Item2;
+ TData adornmentData = spanDataPair.Item3;
+ if (this.adornmentCache.TryGetValue(snapshotSpan, out adornment))
+ {
+ if (UpdateAdornment(adornment, adornmentData))
+ toRemove.Remove(snapshotSpan);
+ }
+ else
+ {
+ adornment = CreateAdornment(adornmentData, snapshotSpan);
+
+ if (adornment == null)
+ continue;
+
+ // Get the adornment to measure itself. Its DesiredSize property is used to determine
+ // how much space to leave between text for this adornment.
+ // Note: If the size of the adornment changes, the line will be reformatted to accommodate it.
+ // Note: Some adornments may change size when added to the view's visual tree due to inherited
+ // dependency properties that affect layout. Such options can include SnapsToDevicePixels,
+ // UseLayoutRounding, TextRenderingMode, TextHintingMode, and TextFormattingMode. Making sure
+ // that these properties on the adornment match the view's values before calling Measure here
+ // can help avoid the size change and the resulting unnecessary re-format.
+ adornment.Measure(new Size(double.PositiveInfinity, double.PositiveInfinity));
+
+ this.adornmentCache.Add(snapshotSpan, adornment);
+ }
+
+ yield return new TagSpan<IntraTextAdornmentTag>(snapshotSpan, new IntraTextAdornmentTag(adornment, null, affinity));
+ }
+
+ foreach (var snapshotSpan in toRemove)
+ this.adornmentCache.Remove(snapshotSpan);
+ }
+
+ public event EventHandler<SnapshotSpanEventArgs> TagsChanged;
+
+ private class Comparer : IEqualityComparer<Tuple<SnapshotSpan, PositionAffinity?, TData>>
+ {
+ public bool Equals(Tuple<SnapshotSpan, PositionAffinity?, TData> x, Tuple<SnapshotSpan, PositionAffinity?, TData> y)
+ {
+ if (x == null && y == null)
+ return true;
+ if (x == null || y == null)
+ return false;
+ return x.Item1.Equals(y.Item1);
+ }
+
+ public int GetHashCode(Tuple<SnapshotSpan, PositionAffinity?, TData> obj)
+ {
+ return obj.Item1.GetHashCode();
+ }
+ }
+
+ }
+}
diff --git a/Source/DafnyExtension/OutliningTagger.cs b/Source/DafnyExtension/OutliningTagger.cs index 99611db8..3bbd0b64 100644 --- a/Source/DafnyExtension/OutliningTagger.cs +++ b/Source/DafnyExtension/OutliningTagger.cs @@ -30,7 +30,7 @@ namespace DafnyLanguage internal IBufferTagAggregatorFactoryService AggregatorFactory = null;
public ITagger<T> CreateTagger<T>(ITextBuffer buffer) where T : ITag {
- ITagAggregator<DafnyResolverTag> tagAggregator = AggregatorFactory.CreateTagAggregator<DafnyResolverTag>(buffer);
+ ITagAggregator<IDafnyResolverTag> tagAggregator = AggregatorFactory.CreateTagAggregator<IDafnyResolverTag>(buffer);
// create a single tagger for each buffer.
Func<ITagger<T>> sc = delegate() { return new OutliningTagger(buffer, tagAggregator) as ITagger<T>; };
return buffer.Properties.GetOrCreateSingletonProperty<ITagger<T>>(sc);
@@ -51,9 +51,9 @@ namespace DafnyLanguage ITextSnapshot _snapshot; // the most recent snapshot of _buffer that we have been informed about
Dafny.Program _program; // the program parsed from _snapshot
List<OutliningRegion> _regions = new List<OutliningRegion>(); // the regions generated from _program
- ITagAggregator<DafnyResolverTag> _aggregator;
+ ITagAggregator<IDafnyResolverTag> _aggregator;
- internal OutliningTagger(ITextBuffer buffer, ITagAggregator<DafnyResolverTag> tagAggregator) {
+ internal OutliningTagger(ITextBuffer buffer, ITagAggregator<IDafnyResolverTag> tagAggregator) {
_buffer = buffer;
_snapshot = _buffer.CurrentSnapshot;
_aggregator = tagAggregator;
diff --git a/Source/DafnyExtension/ProgressMargin.cs b/Source/DafnyExtension/ProgressMargin.cs index 1d8281ad..a96a0373 100644 --- a/Source/DafnyExtension/ProgressMargin.cs +++ b/Source/DafnyExtension/ProgressMargin.cs @@ -23,20 +23,21 @@ namespace DafnyLanguage {
#region UI stuff
+
internal class ProgressMarginGlyphFactory : IGlyphFactory
{
public UIElement GenerateGlyph(IWpfTextViewLine line, IGlyphTag tag) {
- var dtag = tag as ProgressGlyphTag;
- if (dtag == null) {
+ var pgt = tag as ProgressGlyphTag;
+ if (pgt == null) {
return null;
}
- System.Windows.Shapes.Rectangle sh = new Rectangle() {
- Fill = dtag.Val == 0 ? Brushes.Violet : Brushes.DarkOrange,
+ return new Rectangle()
+ {
+ Fill = pgt.Val == 0 ? Brushes.Violet : Brushes.DarkOrange,
Height = 18.0,
Width = 3.0
};
- return sh;
}
}
@@ -59,6 +60,7 @@ namespace DafnyLanguage Val = val;
}
}
+
#endregion
@@ -79,7 +81,7 @@ namespace DafnyLanguage ITextDocumentFactoryService _textDocumentFactory = null;
public ITagger<T> CreateTagger<T>(ITextBuffer buffer) where T : ITag {
- ITagAggregator<DafnyResolverTag> tagAggregator = AggregatorFactory.CreateTagAggregator<DafnyResolverTag>(buffer);
+ ITagAggregator<IDafnyResolverTag> tagAggregator = AggregatorFactory.CreateTagAggregator<IDafnyResolverTag>(buffer);
// create a single tagger for each buffer.
Func<ITagger<T>> sc = delegate() { return new ProgressTagger(buffer, _serviceProvider, tagAggregator, _textDocumentFactory) as ITagger<T>; };
return buffer.Properties.GetOrCreateSingletonProperty<ITagger<T>>(sc);
@@ -100,7 +102,7 @@ namespace DafnyLanguage readonly DispatcherTimer timer;
- public ProgressTagger(ITextBuffer buffer, IServiceProvider serviceProvider, ITagAggregator<DafnyResolverTag> tagAggregator, ITextDocumentFactoryService textDocumentFactory) {
+ public ProgressTagger(ITextBuffer buffer, IServiceProvider serviceProvider, ITagAggregator<IDafnyResolverTag> tagAggregator, ITextDocumentFactoryService textDocumentFactory) {
_buffer = buffer;
if (!textDocumentFactory.TryGetTextDocument(_buffer, out _document))
@@ -357,7 +359,8 @@ namespace DafnyLanguage public event EventHandler<SnapshotSpanEventArgs> TagsChanged;
- IEnumerable<ITagSpan<ProgressGlyphTag>> ITagger<ProgressGlyphTag>.GetTags(NormalizedSnapshotSpanCollection spans) {
+ IEnumerable<ITagSpan<ProgressGlyphTag>> ITagger<ProgressGlyphTag>.GetTags(NormalizedSnapshotSpanCollection spans)
+ {
if (spans.Count == 0) yield break;
var targetSnapshot = spans[0].Snapshot;
diff --git a/Source/DafnyExtension/ResolverTagger.cs b/Source/DafnyExtension/ResolverTagger.cs index aad7217c..7f1a7b4b 100644 --- a/Source/DafnyExtension/ResolverTagger.cs +++ b/Source/DafnyExtension/ResolverTagger.cs @@ -10,9 +10,8 @@ using System.Collections.Concurrent; using System.Collections.Generic;
using System.ComponentModel.Composition;
using System.Diagnostics.Contracts;
-using System.IO;
using System.Linq;
-using EnvDTE;
+using System.Windows.Shapes;
using Microsoft.VisualStudio;
using Microsoft.VisualStudio.Shell;
using Microsoft.VisualStudio.Shell.Interop;
@@ -30,7 +29,7 @@ namespace DafnyLanguage [Export(typeof(ITaggerProvider))]
[ContentType("dafny")]
- [TagType(typeof(DafnyResolverTag))]
+ [TagType(typeof(IDafnyResolverTag))]
internal sealed class ResolverTaggerProvider : ITaggerProvider
{
[Import(typeof(Microsoft.VisualStudio.Shell.SVsServiceProvider))]
@@ -54,22 +53,43 @@ namespace DafnyLanguage #region Tags
- public abstract class DafnyResolverTag : ITag
+ public interface IDafnyResolverTag : ITag
{
}
- public class DafnyErrorResolverTag : DafnyResolverTag
+ public class DafnyErrorResolverTag : ErrorTag, IDafnyResolverTag
{
- public readonly string Typ;
- public readonly string Msg;
- public DafnyErrorResolverTag(string typ, string msg)
+ public DafnyError Error { get; private set; }
+
+ public DafnyErrorResolverTag(DafnyError error)
+ : base(ErrorType(error), error.Message)
+ {
+ Error = error;
+ }
+
+ private static string ErrorType(DafnyError err)
{
- Typ = typ;
- Msg = msg;
+ string ty; // the COLORs below indicate what I see on my machine
+ switch (err.Category)
+ {
+ default: // unexpected category
+ case ErrorCategory.ParseError:
+ case ErrorCategory.ParseWarning:
+ ty = "syntax error"; break; // COLOR: red
+ case ErrorCategory.ResolveError:
+ ty = "compiler error"; break; // COLOR: blue
+ case ErrorCategory.VerificationError:
+ ty = "error"; break; // COLOR: red
+ case ErrorCategory.AuxInformation:
+ ty = "other error"; break; // COLOR: purple red
+ case ErrorCategory.InternalError:
+ ty = "error"; break; // COLOR: red
+ }
+ return ty;
}
}
- public class DafnySuccessResolverTag : DafnyResolverTag
+ public class DafnySuccessResolverTag : IDafnyResolverTag
{
public readonly Dafny.Program Program;
public DafnySuccessResolverTag(Dafny.Program program)
@@ -84,7 +104,7 @@ namespace DafnyLanguage /// <summary>
/// Translate PkgDefTokenTags into ErrorTags and Error List items
/// </summary>
- public sealed class ResolverTagger : ITagger<DafnyResolverTag>, IDisposable
+ public sealed class ResolverTagger : ITagger<IDafnyResolverTag>, IDisposable
{
readonly ITextBuffer _buffer;
readonly ITextDocument _document;
@@ -228,7 +248,7 @@ namespace DafnyLanguage /// <summary>
/// Find the Error tokens in the set of all tokens and create an ErrorTag for each
/// </summary>
- public IEnumerable<ITagSpan<DafnyResolverTag>> GetTags(NormalizedSnapshotSpanCollection spans)
+ public IEnumerable<ITagSpan<IDafnyResolverTag>> GetTags(NormalizedSnapshotSpanCollection spans)
{
if (spans.Count == 0) yield break;
var currentSnapshot = spans[0].Snapshot;
@@ -236,23 +256,7 @@ namespace DafnyLanguage {
if (err.Category != ErrorCategory.ProcessError)
{
- string ty; // the COLORs below indicate what I see on my machine
- switch (err.Category)
- {
- default: // unexpected category
- case ErrorCategory.ParseError:
- case ErrorCategory.ParseWarning:
- ty = "syntax error"; break; // COLOR: red
- case ErrorCategory.ResolveError:
- ty = "compiler error"; break; // COLOR: blue
- case ErrorCategory.VerificationError:
- ty = "error"; break; // COLOR: red
- case ErrorCategory.AuxInformation:
- ty = "other error"; break; // COLOR: purple red
- case ErrorCategory.InternalError:
- ty = "error"; break; // COLOR: red
- }
- yield return new TagSpan<DafnyResolverTag>(err.Span.GetSpan(currentSnapshot), new DafnyErrorResolverTag(ty, err.Message));
+ yield return new TagSpan<IDafnyResolverTag>(err.Span.GetSpan(currentSnapshot), new DafnyErrorResolverTag(err));
}
}
@@ -265,7 +269,7 @@ namespace DafnyLanguage }
if (prog != null)
{
- yield return new TagSpan<DafnyResolverTag>(new SnapshotSpan(snap, 0, snap.Length), new DafnySuccessResolverTag(prog));
+ yield return new TagSpan<IDafnyResolverTag>(new SnapshotSpan(snap, 0, snap.Length), new DafnySuccessResolverTag(prog));
}
}
@@ -345,6 +349,11 @@ namespace DafnyLanguage task.Navigate += new EventHandler(NavigateHandler);
}
_errorProvider.Tasks.Add(task);
+
+ if (err.Model != null)
+ {
+
+ }
}
_errorProvider.ResumeRefresh();
}
@@ -440,6 +449,18 @@ namespace DafnyLanguage public readonly string Message;
public readonly ITrackingSpan Span;
public readonly string Model;
+ public bool IsSelected { get { return SelectedError == this; } }
+ private readonly ErrorSelection _errorSelection;
+ public DafnyError SelectedError { get { return _errorSelection.Error; } set { _errorSelection.Error = value; } }
+ public Shape Adornment;
+
+ internal class ErrorSelection
+ {
+ internal DafnyError Error = null;
+ }
+
+ internal static readonly ErrorSelection _errorSelectionSingleton = new ErrorSelection();
+
/// <summary>
/// "line" and "col" are expected to be 0-based
@@ -455,6 +476,7 @@ namespace DafnyLanguage var sLength = Math.Max(0, Math.Min(sLine.Length - Column, 5));
Span = snapshot.CreateTrackingSpan(sLine.Start + Column, sLength, SpanTrackingMode.EdgeExclusive, TrackingFidelityMode.Forward);
Model = model;
+ _errorSelection = _errorSelectionSingleton;
}
}
diff --git a/Source/DafnyMenu/DafnyMenu.vsct b/Source/DafnyMenu/DafnyMenu.vsct index 25c8dea9..d23ebc7f 100644 --- a/Source/DafnyMenu/DafnyMenu.vsct +++ b/Source/DafnyMenu/DafnyMenu.vsct @@ -108,7 +108,7 @@ <CommandFlag>DynamicVisibility</CommandFlag>
<CommandFlag>DefaultInvisible</CommandFlag>
<Strings>
- <ButtonText>Show error model</ButtonText>
+ <ButtonText>Show model for selected error in BVD</ButtonText>
</Strings>
</Button>
diff --git a/Source/DafnyMenu/DafnyMenuPackage.cs b/Source/DafnyMenu/DafnyMenuPackage.cs index 1506e893..cb32f9fd 100644 --- a/Source/DafnyMenu/DafnyMenuPackage.cs +++ b/Source/DafnyMenu/DafnyMenuPackage.cs @@ -215,7 +215,7 @@ namespace DafnyLanguage.DafnyMenu && DafnyLanguage.ResolverTagger.ResolverTaggers.TryGetValue(dte.ActiveDocument.FullName, out resolver)
&& resolver.Program != null
&& resolver.VerificationErrors.Any(err => !string.IsNullOrEmpty(err.Model));
- showErrorModelCommand.Visible = false; // TODO(wuestholz): Enable this.
+ showErrorModelCommand.Visible = visible;
}
private void ShowErrorModelCallback(object sender, EventArgs e)
@@ -225,7 +225,7 @@ namespace DafnyLanguage.DafnyMenu var show = dte.ActiveDocument != null
&& DafnyLanguage.ResolverTagger.ResolverTaggers.TryGetValue(dte.ActiveDocument.FullName, out resolver)
&& resolver.Program != null
- && resolver.VerificationErrors.Any(err => !string.IsNullOrEmpty(err.Model));
+ && resolver.VerificationErrors.Any(err => err.IsSelected && !string.IsNullOrEmpty(err.Model));
if (show)
{
var window = this.FindToolWindow(typeof(BvdToolWindow), 0, true);
@@ -234,11 +234,10 @@ namespace DafnyLanguage.DafnyMenu throw new NotSupportedException("Can not create BvdToolWindow.");
}
- var models = resolver.VerificationErrors.Select(err => err.Model).Where(m => !string.IsNullOrEmpty(m)).ToArray();
-
- for (int i = 0; i < models.Length; i++)
+ var selectedError = resolver.VerificationErrors.FirstOrDefault(err => err.IsSelected && !string.IsNullOrEmpty(err.Model));
+ if (selectedError != null)
{
- BvdToolWindow.BVD.ReadModel(models[i], i);
+ BvdToolWindow.BVD.ReadModel(selectedError.Model);
}
IVsWindowFrame windowFrame = (IVsWindowFrame)window.Frame;
|