using System; using System.Collections.Generic; using System.ComponentModel.Composition; using System.Linq; using System.Windows; using System.Windows.Controls; 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 = "ProgressTagger")] [TextViewRole(PredefinedTextViewRoles.Document)] [TagType(typeof(IntraTextAdornmentTag))] internal sealed class ErrorModelTaggerProvider : IViewTaggerProvider { [Import] internal IBufferTagAggregatorFactoryService BufferTagAggregatorFactoryService = null; public ITagger CreateTagger(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>( () => BufferTagAggregatorFactoryService.CreateTagAggregator(textView.TextBuffer))) as ITagger; } } #endregion #region Tagger internal sealed class ErrorModelTagger : ITagger, IDisposable { IWpfTextView _view; ITagAggregator _aggregator; internal static ITagger GetTagger(IWpfTextView view, Lazy> aggregator) { return view.Properties.GetOrCreateSingletonProperty( () => new ErrorModelTagger(view, aggregator.Value)); } private ErrorModelTagger(IWpfTextView view, ITagAggregator aggregator) { _view = view; _aggregator = aggregator; _aggregator.TagsChanged += new EventHandler(_aggregator_TagsChanged); } public void Dispose() { _aggregator.Dispose(); _view.Properties.RemoveProperty(typeof(ErrorModelTagger)); } public IEnumerable> GetTags(NormalizedSnapshotSpanCollection spans) { if (spans.Count == 0) yield break; var snapshot = spans[0].Snapshot; var adornmentsPerSnapshot = new Dictionary>(); foreach (var tag in _aggregator.GetTags(spans)) { var ertag = tag.Tag as DafnyErrorResolverTag; if (ertag != null && ertag.Error.ModelText != null) { NormalizedSnapshotSpanCollection normSpans = tag.Span.GetSpans(snapshot); if (normSpans.Count != 1) continue; var adornment = _view.VisualElement.Dispatcher.Invoke(() => CreateErrorAdornment(ertag)); var span = new SnapshotSpan(normSpans[0].Start, 0); List adornments; if (adornmentsPerSnapshot.TryGetValue(span, out adornments)) { adornments.Add(adornment); } else { adornmentsPerSnapshot.Add(span, new List { adornment }); } } var esrtag = tag.Tag as DafnyErrorStateResolverTag; if (esrtag != null) { var adornment = _view.VisualElement.Dispatcher.Invoke(() => CreateErrorStateAdornment(esrtag)); var span = esrtag.Span.GetSpan(snapshot); List adornments; if (adornmentsPerSnapshot.TryGetValue(span, out adornments)) { adornments.Add(adornment); } else { adornmentsPerSnapshot.Add(span, new List { adornment }); } } } foreach (var adornments in adornmentsPerSnapshot) { var panel = _view.VisualElement.Dispatcher.Invoke(() => { var maxConcurrentAdornments = adornments.Value.Where(a => a.Fill == Brushes.Crimson).Count() // number of error adornments + (adornments.Value.Any(a => a.Fill != Brushes.Crimson) ? 1 : 0); // number of error state adornments var p = new StackPanel { Orientation = Orientation.Horizontal, Width = 12.0 * maxConcurrentAdornments, Height = 12.0, }; foreach (var adornment in adornments.Value) { p.Children.Add(adornment); } p.Measure(new Size(double.PositiveInfinity, double.PositiveInfinity)); return p; }); yield return new TagSpan(adornments.Key, new IntraTextAdornmentTag(panel, null, PositionAffinity.Successor)); } } private static string ErrorStateToolTip(bool isSelected, string description) { return string.Format("{0}{1}", isSelected ? "unselect state" : "select state", !string.IsNullOrEmpty(description) ? " [" + description + "]" : ""); } private Ellipse CreateErrorStateAdornment(DafnyErrorStateResolverTag esrtag) { var result = new Ellipse { Fill = Brushes.DodgerBlue, Height = 12.0, Width = 12.0, ToolTip = ErrorStateToolTip(false, esrtag.Description), StrokeThickness = 3.0, Stroke = Brushes.DodgerBlue, Cursor = Cursors.Arrow, Visibility = System.Windows.Visibility.Collapsed }; esrtag.Error.StateChangeEvent += new DafnyError.StateChangeEventHandler((o) => { _view.VisualElement.Dispatcher.Invoke(() => { result.Visibility = esrtag.Error.IsSelected ? System.Windows.Visibility.Visible : System.Windows.Visibility.Collapsed; var isSelected = esrtag.Error.IsSelected && esrtag.Error.SelectedStateId == esrtag.Id; result.Stroke = isSelected ? Brushes.Black : Brushes.DodgerBlue; if (isSelected) { result.ToolTip = ErrorStateToolTip(isSelected, esrtag.Description); esrtag.Error.SelectedStateAdornment = result; } }); }); result.MouseDown += new MouseButtonEventHandler((s, e) => { _view.VisualElement.Dispatcher.Invoke(() => { if (!esrtag.Error.IsSelected) { return; } if (esrtag.Error.SelectedStateAdornment == result) { // unselect it esrtag.Error.SelectedStateAdornment = null; esrtag.Error.SelectedStateId = -1; result.Stroke = Brushes.DodgerBlue; result.ToolTip = result.ToolTip.ToString().Replace("unselect", "select"); } else { // unselect the old one if (esrtag.Error.SelectedStateAdornment != null) { esrtag.Error.SelectedStateAdornment.Stroke = Brushes.DodgerBlue; esrtag.Error.SelectedStateAdornment.ToolTip = esrtag.Error.SelectedStateAdornment.ToolTip.ToString().Replace("unselect", "select"); esrtag.Error.SelectedStateAdornment = null; esrtag.Error.SelectedStateId = -1; } // select the new one esrtag.Error.SelectedStateAdornment = result; esrtag.Error.SelectedStateAdornment.Stroke = Brushes.Black; esrtag.Error.SelectedStateAdornment.ToolTip = ErrorStateToolTip(true, esrtag.Description); esrtag.Error.SelectedStateId = esrtag.Id; if (!string.IsNullOrEmpty(esrtag.Error.ModelText)) { DafnyClassifier.DafnyMenuPackage.ShowErrorModelInBVD(esrtag.Error.ModelText, esrtag.Id); } } }); }); return result; } private Ellipse CreateErrorAdornment(DafnyErrorResolverTag ertag) { var result = new Ellipse { Fill = Brushes.Crimson, Height = 12.0, Width = 12.0, ToolTip = "select error", StrokeThickness = 3.0, Stroke = Brushes.Crimson, Cursor = Cursors.Arrow, }; result.Measure(new Size(double.PositiveInfinity, double.PositiveInfinity)); result.MouseDown += new MouseButtonEventHandler((s, e) => { _view.VisualElement.Dispatcher.Invoke(() => { if (ertag.Error.IsSelected) { // unselect it var selErr = ertag.Error.SelectedError; selErr.SelectedStateId = -1; selErr.SelectedStateAdornment = null; ertag.Error.SelectedError = null; result.Stroke = Brushes.Crimson; result.ToolTip = "select error"; selErr.Notify(); } else { // unselect the old one if (ertag.Error.SelectedError != null) { var selErr = ertag.Error.SelectedError; selErr.SelectedStateId = -1; selErr.SelectedStateAdornment = null; selErr.Adornment.Stroke = Brushes.Crimson; selErr.Adornment.ToolTip = "select error"; ertag.Error.SelectedError = null; selErr.Notify(); } // 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"; if (!string.IsNullOrEmpty(ertag.Error.ModelText)) { // select the last error state ertag.Error.SelectedStateId = ertag.Error.Model.States.Count() - 1; ertag.Error.SelectedStateAdornment = null; DafnyClassifier.DafnyMenuPackage.ShowErrorModelInBVD(ertag.Error.ModelText, ertag.Error.SelectedStateId); } ertag.Error.SelectedError.Notify(); } }); }); return result; } public event EventHandler TagsChanged; void _aggregator_TagsChanged(object sender, TagsChangedEventArgs e) { var chng = TagsChanged; if (chng != null) { NormalizedSnapshotSpanCollection spans = e.Span.GetSpans(_view.TextBuffer.CurrentSnapshot); if (spans.Count > 0) { SnapshotSpan span = new SnapshotSpan(spans[0].Start, spans[spans.Count - 1].End); _view.VisualElement.Dispatcher.Invoke(() => { chng(this, new SnapshotSpanEventArgs(span)); }); } } } } #endregion }