From 57e91b54c99238bfcc40880f8ecbaf590d4030cf Mon Sep 17 00:00:00 2001
From: Unknown <leino@LEINO6.redmond.corp.microsoft.com>
Date: Wed, 15 Aug 2012 16:40:36 -0700
Subject: Dafny: fixed some bugs in the newly added DafnyExtension code

---
 Util/VS2010/DafnyExtension/DafnyExtension/HoverText.cs     | 14 +++-----------
 .../DafnyExtension/DafnyExtension/IdentifierTagger.cs      |  5 +++++
 2 files changed, 8 insertions(+), 11 deletions(-)

(limited to 'Util')

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);
-- 
cgit v1.2.3