Dafny VS Extension: edited to make it build with new AST types, fixed some bugs, added a temporary progress indicator

6 files changed, 143 insertions, 26 deletions

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<Dafny.ModuleDecl> modules = new List<Dafny.ModuleDecl>();

+      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 @@
     <Reference Include="Houdini">

       <HintPath>..\..\..\..\Binaries\Houdini.dll</HintPath>

     </Reference>

-    <Reference Include="Microsoft.Contracts, Version=1.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">

-      <SpecificVersion>False</SpecificVersion>

-      <HintPath>..\..\..\..\Binaries\Microsoft.Contracts.dll</HintPath>

-    </Reference>

     <Reference Include="Model">

       <HintPath>..\..\..\..\Binaries\Model.dll</HintPath>

     </Reference>

@@ -129,6 +125,7 @@
   </ItemGroup>

   <ItemGroup>

     <Compile Include="BufferIdleEventUtil.cs" />

+    <Compile Include="ProgressMargin.cs" />

     <Compile Include="OutliningTagger.cs" />

     <Compile Include="ResolverTagger.cs" />

     <Compile Include="DafnyDriver.cs" />

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<IOutliningRegionTag>

   {

     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<ORegion> _regions = new List<ORegion>();  // the regions generated from _program

     ITagAggregator<DafnyResolverTag> _aggregator;

-    Dafny.Program _program;

-    List<ORegion> _regions = new List<ORegion>();

 

     internal OutliningTagger(ITextBuffer buffer, ITagAggregator<DafnyResolverTag> tagAggregator) {

       _buffer = buffer;

+      _snapshot = _buffer.CurrentSnapshot;

       _aggregator = tagAggregator;

       _aggregator.TagsChanged += new EventHandler<TagsChangedEventArgs>(_aggregator_TagsChanged);

     }

@@ -60,11 +63,26 @@ namespace DafnyLanguage
     /// </summary>

     public IEnumerable<ITagSpan<IOutliningRegionTag>> 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<OutliningRegionTag>(

-          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<OutliningRegionTag>(

+            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<ORegion> newRegions = new List<ORegion>();

 

-      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<ProgressGlyphTag>

+  {

+    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<ITagSpan<ProgressGlyphTag>> ITagger<ProgressGlyphTag>.GetTags(NormalizedSnapshotSpanCollection spans) {

+      if (spans.Count == 0) yield break;

+      if (spans[0].Snapshot.Version != latestClearedVersion) {

+        foreach (SnapshotSpan span in spans) {

+          yield return new TagSpan<ProgressGlyphTag>(new SnapshotSpan(span.Start, span.Length), new ProgressGlyphTag(1));

+        }

+      }

+    }

+    public event EventHandler<SnapshotSpanEventArgs> TagsChanged;

+  }

+

+  [Export(typeof(ITaggerProvider))]

+  [ContentType("dafny")]

+  [TagType(typeof(ProgressGlyphTag))]

+  class ProgressTaggerProvider : ITaggerProvider

+  {

+    public ITagger<T> CreateTagger<T>(ITextBuffer buffer) where T : ITag {

+      return new ProgressTagger(buffer) as ITagger<T>;

+    }

+  }

+}

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<DafnyError> _errors = new List<DafnyError>();

+    public ITextSnapshot _snapshot;  // may be null

+    List<DafnyError> _errors = new List<DafnyError>();  // 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
     /// </summary>

     public IEnumerable<ITagSpan<DafnyResolverTag>> 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<DafnyResolverTag>(new SnapshotSpan(snapshot, 0, snapshot.Length), new DafnySuccessResolverTag(_program));

+        yield return new TagSpan<DafnyResolverTag>(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));

+        }

       }

     }