diff options
| author |  leino <unknown> | 2015-11-05 05:18:50 -0800 |
|---|---|---|
| committer | leino <unknown> | 2015-11-05 05:18:50 -0800 |
| commit | 78d8881d6b579e14005a0a520ada8ded698c904e (patch) | |
| tree | 1bf54e0a9480608a1b1c5392e4f51498e6be188d | |
| parent | ab999651fc184fdc6a0cb4b52d1253e6c4b9a060 (diff) | |
In the VS IDE, don't generate hover-text information for auto-generated identifiers
| -rw-r--r-- | Source/DafnyExtension/IdentifierTagger.cs | 10 | ||||
| -rw-r--r-- | 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));
}
}
|