From c6c0e00cd3e104556bcf3c87aa3bf21edecc9ba7 Mon Sep 17 00:00:00 2001 From: Unknown Date: Thu, 2 Aug 2012 13:35:52 -0700 Subject: Dafny VS Extension: edited to make it build with new AST types, fixed some bugs, added a temporary progress indicator --- .../DafnyExtension/DafnyExtension/DafnyDriver.cs | 6 +- .../DafnyExtension/DafnyExtension.csproj | 5 +- .../DafnyExtension/OutliningTagger.cs | 39 +++++++-- .../DafnyExtension/ProgressMargin.cs | 98 ++++++++++++++++++++++ .../DafnyExtension/ResolverTagger.cs | 14 ++-- .../DafnyExtension/DafnyExtension/TokenTagger.cs | 7 +- 6 files changed, 143 insertions(+), 26 deletions(-) create mode 100644 Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs (limited to 'Util') diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs index f24aee55..f5f41e2c 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs +++ b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs @@ -125,12 +125,12 @@ namespace DafnyLanguage } bool ParseAndTypeCheck() { - List modules = new List(); + Dafny.ModuleDecl module = new Dafny.LiteralModuleDecl(new Dafny.DefaultModuleDecl(), null); Dafny.BuiltIns builtIns = new Dafny.BuiltIns(); - int errorCount = Dafny.Parser.Parse(_programText, _filename, modules, builtIns, new VSErrors(this)); + int errorCount = Dafny.Parser.Parse(_programText, _filename, module, builtIns, new VSErrors(this)); if (errorCount != 0) return false; - Dafny.Program program = new Dafny.Program(_filename, modules, builtIns); + Dafny.Program program = new Dafny.Program(_filename, module, builtIns); Dafny.Resolver r = new VSResolver(program, this); r.ResolveProgram(program); diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj index cf33e5a0..4e9dbdf8 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj +++ b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj @@ -63,10 +63,6 @@ ..\..\..\..\Binaries\Houdini.dll - - False - ..\..\..\..\Binaries\Microsoft.Contracts.dll - ..\..\..\..\Binaries\Model.dll @@ -129,6 +125,7 @@ + diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs index 390ed01f..3dcaf1cf 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs +++ b/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs @@ -18,6 +18,7 @@ using Microsoft.VisualStudio.Text.Editor; using Microsoft.VisualStudio.Text.Tagging; using Microsoft.VisualStudio.Text.Projection; using Microsoft.VisualStudio.Utilities; +using System.Diagnostics.Contracts; using Bpl = Microsoft.Boogie; using Dafny = Microsoft.Dafny; @@ -45,12 +46,14 @@ namespace DafnyLanguage internal sealed class OutliningTagger : ITagger { ITextBuffer _buffer; + ITextSnapshot _snapshot; // the most recent snapshot of _buffer that we have been informed about + Dafny.Program _program; // the program parsed from _snapshot + List _regions = new List(); // the regions generated from _program ITagAggregator _aggregator; - Dafny.Program _program; - List _regions = new List(); internal OutliningTagger(ITextBuffer buffer, ITagAggregator tagAggregator) { _buffer = buffer; + _snapshot = _buffer.CurrentSnapshot; _aggregator = tagAggregator; _aggregator.TagsChanged += new EventHandler(_aggregator_TagsChanged); } @@ -60,11 +63,26 @@ namespace DafnyLanguage /// public IEnumerable> GetTags(NormalizedSnapshotSpanCollection spans) { if (spans.Count == 0) yield break; - var snapshot = spans[0].Snapshot; + // (A NormalizedSnapshotSpanCollection contains spans that all come from the same snapshot.) + // The spans are ordered by the .Start component, and the collection contains no adjacent or abutting spans. + // Hence, to find a span that includes all the ones in "spans", we only need to look at the .Start for the + // first spand and the .End of the last span: + var startPoint = spans[0].Start; + var endPoint = spans[spans.Count - 1].End; + + // Note, (startPoint,endPoint) are points in the spans for which we're being asked to provide tags. We need to translate + // these back into the most recent snapshot that we've computed regions for, namely _snapshot. + var entire = new SnapshotSpan(startPoint, endPoint).TranslateTo(_snapshot, SpanTrackingMode.EdgeExclusive); + int start = entire.Start; + int end = entire.End; + if (start == end) yield break; + foreach (var r in _regions) { - yield return new TagSpan( - new SnapshotSpan(snapshot, r.Start, r.Length), - new OutliningRegionTag(false, false, "...", r.HoverText)); + if (r.Start <= end && start <= r.Start + r.Length) { + yield return new TagSpan( + new SnapshotSpan(_snapshot, r.Start, r.Length), + new OutliningRegionTag(false, false, "...", r.HoverText)); + } } } @@ -74,7 +92,7 @@ namespace DafnyLanguage void _aggregator_TagsChanged(object sender, TagsChangedEventArgs e) { var r = sender as ResolverTagger; if (r != null && r._program != null) { - if (!ComputeOutliningRegions(r._program)) + if (!ComputeOutliningRegions(r._program, r._snapshot)) return; // no new regions var chng = TagsChanged; @@ -88,13 +106,15 @@ namespace DafnyLanguage } } - bool ComputeOutliningRegions(Dafny.Program program) { + bool ComputeOutliningRegions(Dafny.Program program, ITextSnapshot snapshot) { + Contract.Requires(snapshot != null); + if (program == _program) return false; // no new regions List newRegions = new List(); - foreach (Dafny.ModuleDecl module in program.Modules) { + foreach (var module in program.Modules) { if (!module.IsDefaultModule) { newRegions.Add(new ORegion(module, "module")); } @@ -117,6 +137,7 @@ namespace DafnyLanguage } } } + _snapshot = snapshot; _regions = newRegions; _program = program; return true; diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs b/Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs new file mode 100644 index 00000000..a4f232dd --- /dev/null +++ b/Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs @@ -0,0 +1,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 + { + 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> ITagger.GetTags(NormalizedSnapshotSpanCollection spans) { + if (spans.Count == 0) yield break; + if (spans[0].Snapshot.Version != latestClearedVersion) { + foreach (SnapshotSpan span in spans) { + yield return new TagSpan(new SnapshotSpan(span.Start, span.Length), new ProgressGlyphTag(1)); + } + } + } + public event EventHandler TagsChanged; + } + + [Export(typeof(ITaggerProvider))] + [ContentType("dafny")] + [TagType(typeof(ProgressGlyphTag))] + class ProgressTaggerProvider : ITaggerProvider + { + public ITagger CreateTagger(ITextBuffer buffer) where T : ITag { + return new ProgressTagger(buffer) as ITagger; + } + } +} diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs index 1a288ab4..05a83b12 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs +++ b/Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs @@ -18,6 +18,7 @@ using Microsoft.VisualStudio.Text.Editor; using Microsoft.VisualStudio.Text.Tagging; using Microsoft.VisualStudio.Text.Projection; using Microsoft.VisualStudio.Utilities; +using System.Diagnostics.Contracts; using Dafny = Microsoft.Dafny; namespace DafnyLanguage @@ -67,8 +68,8 @@ namespace DafnyLanguage { ITextBuffer _buffer; ITextDocument _document; - ITextSnapshot _snapshot; // may be null - List _errors = new List(); + public ITextSnapshot _snapshot; // may be null + List _errors = new List(); // if nonempty, then _snapshot is the snapshot from which the errors were produced ErrorListProvider _errorProvider; public Dafny.Program _program; // non-null only if the snapshot contains a Dafny program that type checks @@ -99,14 +100,13 @@ namespace DafnyLanguage /// public IEnumerable> GetTags(NormalizedSnapshotSpanCollection spans) { if (spans.Count == 0) yield break; - var snapshot = spans[0].Snapshot; - foreach (var err in _errors) { if (err.Category != ErrorCategory.ProcessError) { - var line = snapshot.GetLineFromLineNumber(err.Line); + var line = _snapshot.GetLineFromLineNumber(err.Line); + Contract.Assert(err.Column <= line.Length); var length = line.Length - err.Column; if (5 < length) length = 5; - SnapshotSpan span = new SnapshotSpan(new SnapshotPoint(snapshot, line.Start.Position + err.Column), length); + var span = new SnapshotSpan(new SnapshotPoint(_snapshot, line.Start.Position + err.Column), length); // http://msdn.microsoft.com/en-us/library/dd885244.aspx says one can use the error types below, but they // all show as purple squiggles for me. And just "error" (which is not mentioned on that page) shows up // as red. @@ -127,7 +127,7 @@ namespace DafnyLanguage } } if (_program != null) { - yield return new TagSpan(new SnapshotSpan(snapshot, 0, snapshot.Length), new DafnySuccessResolverTag(_program)); + yield return new TagSpan(new SnapshotSpan(_snapshot, 0, _snapshot.Length), new DafnySuccessResolverTag(_program)); } } diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs index 80976499..e7ce830e 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs +++ b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs @@ -113,10 +113,11 @@ namespace DafnyLanguage _snapshot = snapshot; _regions = newRegions; - foreach (var span in difference) { - var chng = TagsChanged; - if (chng != null) + var chng = TagsChanged; + if (chng != null) { + foreach (var span in difference) { chng(this, new SnapshotSpanEventArgs(span)); + } } } -- cgit v1.2.3