From 368eb2394164425718488b0a79b3ecf551566775 Mon Sep 17 00:00:00 2001 From: Unknown Date: Thu, 30 Aug 2012 14:18:47 -0700 Subject: DafnyExtension: changed how "_" is displayed (now display as a keyword, not as an identifier definition) --- .../DafnyExtension/IdentifierTagger.cs | 21 +++++++++++++++++---- 1 file changed, 17 insertions(+), 4 deletions(-) (limited to 'Util') diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs index c2362a72..7dbf5402 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs +++ b/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs @@ -77,9 +77,21 @@ namespace DafnyLanguage int end = entire.End; foreach (var r in _regions) { if (0 <= r.Length && r.Start <= end && start <= r.Start + r.Length) { + DafnyTokenKinds kind; + switch (r.Kind) { + case IdRegion.OccurrenceKind.Use: + kind = DafnyTokenKinds.VariableIdentifier; break; + case IdRegion.OccurrenceKind.Definition: + kind = DafnyTokenKinds.VariableIdentifierDefinition; break; + case IdRegion.OccurrenceKind.WildDefinition: + kind = DafnyTokenKinds.Keyword; break; + default: + Contract.Assert(false); // unexpected OccurrenceKind + goto case IdRegion.OccurrenceKind.Use; // to please compiler + } yield return new TagSpan( new SnapshotSpan(_snapshot, r.Start, r.Length), - new DafnyTokenTag(r.IsDefinition ? DafnyTokenKinds.VariableIdentifierDefinition : DafnyTokenKinds.VariableIdentifier, r.HoverText)); + new DafnyTokenTag(kind, r.HoverText)); } } } @@ -270,7 +282,8 @@ namespace DafnyLanguage public readonly int Start; public readonly int Length; public readonly string HoverText; - public readonly bool IsDefinition; + public enum OccurrenceKind { Use, Definition, WildDefinition } + public readonly OccurrenceKind Kind; public static void Add(List regions, Bpl.IToken tok, IVariable v, bool isDefinition, ModuleDefinition context) { Contract.Requires(regions != null); @@ -305,7 +318,7 @@ namespace DafnyLanguage kind = formal.InParam ? "in-parameter" : "out-parameter"; } HoverText = string.Format("({2}{3}) {0}: {1}", v.DisplayName, v.Type.TypeName(context), v.IsGhost ? "ghost " : "", kind); - IsDefinition = isDefinition; + Kind = !isDefinition ? OccurrenceKind.Use : VarDecl.HasWildcardName(v) ? OccurrenceKind.WildDefinition : OccurrenceKind.Definition; } private IdRegion(Bpl.IToken tok, Field decl, string kind, bool isDefinition, ModuleDefinition context) { Contract.Requires(tok != null); @@ -314,7 +327,7 @@ namespace DafnyLanguage Start = tok.pos; Length = decl.Name.Length; HoverText = string.Format("({2}{3}) {0}: {1}", decl.FullNameInContext(context), decl.Type.TypeName(context), decl.IsGhost ? "ghost " : "", kind); - IsDefinition = isDefinition; + Kind = !isDefinition ? OccurrenceKind.Use : OccurrenceKind.Definition; } } } -- cgit v1.2.3