Dafny: fixed some bugs in the newly added DafnyExtension code

3 files changed, 13 insertions, 14 deletions

diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs
index 223e0b28..f342ecca 100644
--- a/Dafny/DafnyAst.cs
+++ b/Dafny/DafnyAst.cs
@@ -1818,9 +1818,11 @@ namespace Microsoft.Dafny {
     }

     public override IEnumerable<Expression> SubExpressions {

       get {

-        foreach (var rhs in rhss) {

-          foreach (var ee in rhs.SubExpressions) {

-            yield return ee;

+        if (rhss != null) {

+          foreach (var rhs in rhss) {

+            foreach (var ee in rhs.SubExpressions) {

+              yield return ee;

+            }

           }

         }

       }

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/HoverText.cs b/Util/VS2010/DafnyExtension/DafnyExtension/HoverText.cs
index de0721ec..be806f5b 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/HoverText.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/HoverText.cs
@@ -24,18 +24,16 @@ namespace DafnyLanguage
     IBufferTagAggregatorFactoryService aggService = null;

 

     public IQuickInfoSource TryCreateQuickInfoSource(ITextBuffer textBuffer) {

-      return new OokQuickInfoSource(textBuffer, aggService.CreateTagAggregator<DafnyTokenTag>(textBuffer));

+      return new DafnyQuickInfoSource(textBuffer, aggService.CreateTagAggregator<DafnyTokenTag>(textBuffer));

     }

   }

 

-  class OokQuickInfoSource : IQuickInfoSource

+  class DafnyQuickInfoSource : IQuickInfoSource

   {

     private ITagAggregator<DafnyTokenTag> _aggregator;

     private ITextBuffer _buffer;

-    private bool _disposed = false;

 

-

-    public OokQuickInfoSource(ITextBuffer buffer, ITagAggregator<DafnyTokenTag> aggregator) {

+    public DafnyQuickInfoSource(ITextBuffer buffer, ITagAggregator<DafnyTokenTag> aggregator) {

       _aggregator = aggregator;

       _buffer = buffer;

     }

@@ -43,11 +41,7 @@ namespace DafnyLanguage
     public void AugmentQuickInfoSession(IQuickInfoSession session, IList<object> quickInfoContent, out ITrackingSpan applicableToSpan) {

       applicableToSpan = null;

 

-      if (_disposed)

-        throw new ObjectDisposedException("TestQuickInfoSource");

-

       var triggerPoint = (SnapshotPoint)session.GetTriggerPoint(_buffer.CurrentSnapshot);

-

       if (triggerPoint == null)

         return;

 

@@ -60,9 +54,7 @@ namespace DafnyLanguage
         }

       }

     }

-

     public void Dispose() {

-      _disposed = true;

     }

   }

   // --------------------------------- QuickInfo controller ------------------------------------------

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs
index ab2bc790..bec65954 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs
@@ -192,6 +192,11 @@ namespace DafnyLanguage
         foreach (var kase in e.Cases) {

           kase.Arguments.ForEach(bv => regions.Add(new IdRegion(bv.tok, bv, true)));

         }

+      } else if (expr is Dafny.ChainingExpression) {

+        var e = (Dafny.ChainingExpression)expr;

+        // Do the subexpressions only once (that is, avoid the duplication that occurs in the desugared form of the ChainingExpression)

+        e.Operands.ForEach(ee => ExprRegions(ee, regions));

+        return;  // return here, so as to avoid doing the subexpressions below

       }

       foreach (var ee in expr.SubExpressions) {

         ExprRegions(ee, regions);