From 78d8881d6b579e14005a0a520ada8ded698c904e Mon Sep 17 00:00:00 2001
From: leino <unknown>
Date: Thu, 5 Nov 2015 05:18:50 -0800
Subject: In the VS IDE, don't generate hover-text information for
 auto-generated identifiers

---
 Source/DafnyExtension/IdentifierTagger.cs | 10 +++++-----
 Source/DafnyExtension/OutliningTagger.cs  |  2 +-
 2 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/Source/DafnyExtension/IdentifierTagger.cs b/Source/DafnyExtension/IdentifierTagger.cs
index 51f837f7..998a2d7f 100644
--- a/Source/DafnyExtension/IdentifierTagger.cs
+++ b/Source/DafnyExtension/IdentifierTagger.cs
@@ -381,7 +381,7 @@ namespace DafnyLanguage
         Contract.Requires(prog != null);
         Contract.Requires(tok != null);
         Contract.Requires(v != null);
-        if (InMainFile(prog, tok)) {
+        if (InMainFileAndUserDefined(prog, tok)) {
           regions.Add(new IdRegion(tok, v, isDefinition, kind, context));
         }
       }
@@ -391,7 +391,7 @@ namespace DafnyLanguage
         Contract.Requires(tok != null);
         Contract.Requires(decl != null);
         Contract.Requires(kind != null);
-        if (InMainFile(prog, tok)) {
+        if (InMainFileAndUserDefined(prog, tok)) {
           regions.Add(new IdRegion(tok, decl, showType, kind, isDefinition, context));
         }
       }
@@ -401,7 +401,7 @@ namespace DafnyLanguage
         Contract.Requires(prog != null);
         Contract.Requires(tok != null);
         Contract.Requires(text != null);
-        if (InMainFile(prog, tok)) {
+        if (InMainFileAndUserDefined(prog, tok)) {
           regions.Add(new IdRegion(tok, OccurrenceKind.AdditionalInformation, text, length));
         }
       }
@@ -457,10 +457,10 @@ namespace DafnyLanguage
 
   public abstract class DafnyRegion
   {
-    public static bool InMainFile(Microsoft.Dafny.Program prog, Bpl.IToken tok) {
+    public static bool InMainFileAndUserDefined(Microsoft.Dafny.Program prog, Bpl.IToken tok) {
       Contract.Requires(prog != null);
       Contract.Requires(tok != null);
-      return object.Equals(prog.FullName, tok.filename);
+      return object.Equals(prog.FullName, tok.filename) && !(tok is AutoGeneratedToken);
     }
   }
 
diff --git a/Source/DafnyExtension/OutliningTagger.cs b/Source/DafnyExtension/OutliningTagger.cs
index ea611594..fc06d4bf 100644
--- a/Source/DafnyExtension/OutliningTagger.cs
+++ b/Source/DafnyExtension/OutliningTagger.cs
@@ -201,7 +201,7 @@ namespace DafnyLanguage
       public static void Add(List<OutliningRegion> regions, Microsoft.Dafny.Program prog, Dafny.INamedRegion decl, string kind) {
         Contract.Requires(regions != null);
         Contract.Requires(prog != null);
-        if (InMainFile(prog, decl.BodyStartTok)) {
+        if (InMainFileAndUserDefined(prog, decl.BodyStartTok)) {
           regions.Add(new OutliningRegion(decl, kind));
         }
       }
-- 
cgit v1.2.3