diff options
| -rw-r--r-- | Source/Dafny/Reporting.cs | 13 | ||||
| -rw-r--r-- | Source/DafnyExtension/IdentifierTagger.cs | 21 |
2 files changed, 7 insertions, 27 deletions
diff --git a/Source/Dafny/Reporting.cs b/Source/Dafny/Reporting.cs index 77869d9f..63ec520a 100644 --- a/Source/Dafny/Reporting.cs +++ b/Source/Dafny/Reporting.cs @@ -34,21 +34,14 @@ namespace Microsoft.Dafny { AllMessages[ErrorLevel.Info] = new List<ErrorMessage>();
}
- protected bool ShouldDiscard(MessageSource source, ErrorLevel level) {
- return ((ErrorsOnly && level != ErrorLevel.Error) ||
- (!DafnyOptions.O.PrintTooltips && level == ErrorLevel.Info));
- }
-
// This is the only thing that needs to be overriden
public virtual bool Message(MessageSource source, ErrorLevel level, IToken tok, string msg) {
- var discard = ShouldDiscard(source, level);
-
+ bool discard = (ErrorsOnly && level != ErrorLevel.Error) || // Discard non-errors if ErrorsOnly is set
+ (tok is TokenWrapper && !(tok is NestedToken)); // Discard wrapped tokens, except for nested ones
if (!discard) {
AllMessages[level].Add(new ErrorMessage { token = tok, message = msg });
- return true;
}
-
- return false;
+ return !discard;
}
public int Count(ErrorLevel level) {
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<IdRegion> newRegions = new List<IdRegion>();
- 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<IdRegion> 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<IdRegion> 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<IdRegion> 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) {
|