From 9358a72360d50688fc3d32abc30f522ec97c39e6 Mon Sep 17 00:00:00 2001
From: Unknown <leino@LEINO6.redmond.corp.microsoft.com>
Date: Thu, 30 Aug 2012 14:07:34 -0700
Subject: Dafny: allow "_" as don't-care variable name

---
 Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'Util')

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