From 75e436019003604ea3118a13ccd9b6ea079c643f Mon Sep 17 00:00:00 2001 From: Clément Pit--Claudel Date: Thu, 20 Aug 2015 11:52:32 -0700 Subject: Discard error messages that refer to a non-nested TokenWrapper. The VS extension already did that, but it also filtered out nested tokens. That prevented info about triggers from being reported. Other interfaces (the CLI and Emacs, in particular) should have the same ability. Surprinsingly, this doesn't cause any tests failures. --- Source/DafnyExtension/IdentifierTagger.cs | 21 ++++----------------- 1 file changed, 4 insertions(+), 17 deletions(-) (limited to 'Source/DafnyExtension') diff --git a/Source/DafnyExtension/IdentifierTagger.cs b/Source/DafnyExtension/IdentifierTagger.cs index 13991496..5b70329d 100644 --- a/Source/DafnyExtension/IdentifierTagger.cs +++ b/Source/DafnyExtension/IdentifierTagger.cs @@ -15,7 +15,6 @@ using Microsoft.VisualStudio.Text.Tagging; using Microsoft.VisualStudio.Utilities; using Bpl = Microsoft.Boogie; - namespace DafnyLanguage { @@ -136,8 +135,7 @@ namespace DafnyLanguage List newRegions = new List(); - foreach (var info in program.reporter.AllMessages[ErrorLevel.Info]) - { + foreach (var info in program.reporter.AllMessages[ErrorLevel.Info]) { IdRegion.Add(newRegions, info.token, info.message, info.token.val.Length); } @@ -368,11 +366,6 @@ namespace DafnyLanguage public readonly OccurrenceKind Kind; public readonly IVariable Variable; - static bool SurfaceSyntaxToken(Bpl.IToken tok) { - Contract.Requires(tok != null); - return !(tok is TokenWrapper); - } - public static void Add(List regions, Bpl.IToken tok, IVariable v, bool isDefinition, ModuleDefinition context) { Contract.Requires(regions != null); Contract.Requires(tok != null); @@ -383,27 +376,21 @@ namespace DafnyLanguage Contract.Requires(regions != null); Contract.Requires(tok != null); Contract.Requires(v != null); - if (SurfaceSyntaxToken(tok)) { - regions.Add(new IdRegion(tok, v, isDefinition, kind, context)); - } + regions.Add(new IdRegion(tok, v, isDefinition, kind, context)); } public static void Add(List regions, Bpl.IToken tok, Field decl, Microsoft.Dafny.Type showType, string kind, bool isDefinition, ModuleDefinition context) { Contract.Requires(regions != null); Contract.Requires(tok != null); Contract.Requires(decl != null); Contract.Requires(kind != null); - if (SurfaceSyntaxToken(tok)) { - regions.Add(new IdRegion(tok, decl, showType, kind, isDefinition, context)); - } + regions.Add(new IdRegion(tok, decl, showType, kind, isDefinition, context)); } public static void Add(List regions, Bpl.IToken tok, string text, int length) { Contract.Requires(regions != null); Contract.Requires(tok != null); Contract.Requires(text != null); - if (SurfaceSyntaxToken(tok)) { - regions.Add(new IdRegion(tok, OccurrenceKind.AdditionalInformation, text, length)); - } + regions.Add(new IdRegion(tok, OccurrenceKind.AdditionalInformation, text, length)); } private IdRegion(Bpl.IToken tok, IVariable v, bool isDefinition, string kind, ModuleDefinition context) { -- cgit v1.2.3