summaryrefslogtreecommitdiff
path: root/Util/VS2010
diff options
context:
space:
mode:
authorGravatar Unknown <leino@LEINO6.redmond.corp.microsoft.com>2012-08-30 17:01:55 -0700
committerGravatar Unknown <leino@LEINO6.redmond.corp.microsoft.com>2012-08-30 17:01:55 -0700
commit76d973603cfe04d534a332cf83d18dca7dc228ad (patch)
treefc08d3fb4aa043a327ef29477c9d674743970110 /Util/VS2010
parent79c71bc05d7be3c667642aefc21506785175afed (diff)
DafnyExtension: don't duplicate names of inherited identifiers
Diffstat (limited to 'Util/VS2010')
-rw-r--r--Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs9
1 files changed, 7 insertions, 2 deletions
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs
index 7dbf5402..80a6dbb5 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs
@@ -285,11 +285,16 @@ namespace DafnyLanguage
public enum OccurrenceKind { Use, Definition, WildDefinition }
public readonly OccurrenceKind Kind;
+ static bool SurfaceSyntaxToken(Bpl.IToken tok) {
+ Contract.Requires(tok != null);
+ return !(tok is TokenWrapper);
+ }
+
public static void Add(List<IdRegion> regions, Bpl.IToken tok, IVariable v, bool isDefinition, ModuleDefinition context) {
Contract.Requires(regions != null);
Contract.Requires(tok != null);
Contract.Requires(v != null);
- if (!(tok is AutoGeneratedToken)) {
+ if (SurfaceSyntaxToken(tok)) {
regions.Add(new IdRegion(tok, v, isDefinition, context));
}
}
@@ -298,7 +303,7 @@ namespace DafnyLanguage
Contract.Requires(tok != null);
Contract.Requires(decl != null);
Contract.Requires(kind != null);
- if (!(tok is AutoGeneratedToken)) {
+ if (SurfaceSyntaxToken(tok)) {
regions.Add(new IdRegion(tok, decl, kind, isDefinition, context));
}
}