diff options
author | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-08-30 14:07:34 -0700 |
---|---|---|
committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-08-30 14:07:34 -0700 |
commit | 71b527bf4084763bb48c5c9fc44fc2ee456415d6 (patch) | |
tree | d9995be1ff1a5495af6d1810cc4f3616e0e85c71 /Util | |
parent | dce966347df8c56502145cf681a8df4d3a2d9e7b (diff) |
Dafny: allow "_" as don't-care variable name
Diffstat (limited to 'Util')
-rw-r--r-- | Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs index 7aaf8944..c2362a72 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs +++ b/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs @@ -294,7 +294,7 @@ namespace DafnyLanguage Contract.Requires(tok != null);
Contract.Requires(v != null);
Start = tok.pos;
- Length = v.Name.Length;
+ Length = v.DisplayName.Length;
string kind;
if (v is VarDecl) {
kind = "local variable";
@@ -304,7 +304,7 @@ namespace DafnyLanguage var formal = (Formal)v;
kind = formal.InParam ? "in-parameter" : "out-parameter";
}
- HoverText = string.Format("({2}{3}) {0}: {1}", v.Name, v.Type.TypeName(context), v.IsGhost ? "ghost " : "", kind);
+ HoverText = string.Format("({2}{3}) {0}: {1}", v.DisplayName, v.Type.TypeName(context), v.IsGhost ? "ghost " : "", kind);
IsDefinition = isDefinition;
}
private IdRegion(Bpl.IToken tok, Field decl, string kind, bool isDefinition, ModuleDefinition context) {
|