summaryrefslogtreecommitdiff
path: root/Source/DafnyExtension/ResolverTagger.cs
diff options
context:
space:
mode:
authorGravatar wuestholz <unknown>2014-09-22 17:37:04 +0200
committerGravatar wuestholz <unknown>2014-09-22 17:37:04 +0200
commitfc9efd04b96896b6c4bbb94bdfa494787d23b0a4 (patch)
tree4e04dbc3d9621583e9527d9cf76f2274d1d9da14 /Source/DafnyExtension/ResolverTagger.cs
parent962a78676767259bb40eb3e602974bd3c05a6589 (diff)
DafnyExtension: minor change
Diffstat (limited to 'Source/DafnyExtension/ResolverTagger.cs')
-rw-r--r--Source/DafnyExtension/ResolverTagger.cs6
1 files changed, 3 insertions, 3 deletions
diff --git a/Source/DafnyExtension/ResolverTagger.cs b/Source/DafnyExtension/ResolverTagger.cs
index df7878c4..bbe51665 100644
--- a/Source/DafnyExtension/ResolverTagger.cs
+++ b/Source/DafnyExtension/ResolverTagger.cs
@@ -327,7 +327,7 @@ namespace DafnyLanguage
}
catch (Exception e)
{
- newErrors = new List<DafnyError> { new DafnyError(filename, 0, 0, ErrorCategory.InternalError, "internal Dafny error: " + e.Message, snapshot) };
+ newErrors = new List<DafnyError> { new DafnyError(filename, 0, 0, ErrorCategory.InternalError, "internal Dafny error: " + e.Message, snapshot, false) };
program = null;
}
@@ -575,13 +575,13 @@ namespace DafnyLanguage
/// <summary>
/// "line" and "col" are expected to be 0-based
/// </summary>
- public DafnyError(string filename, int line, int col, ErrorCategory cat, string msg, ITextSnapshot snapshot, string model = null, bool inCurrentDocument=true)
+ public DafnyError(string filename, int line, int col, ErrorCategory cat, string msg, ITextSnapshot snapshot, bool isRecycled, string model = null, bool inCurrentDocument = true)
{
Filename = filename;
Line = Math.Max(0, line);
Column = Math.Max(0, col);
Category = cat;
- Message = msg;
+ Message = msg + ((isRecycled && cat == ErrorCategory.VerificationError) ? " (recycled)" : "");
Snapshot = snapshot;
if (inCurrentDocument) {
var sLine = snapshot.GetLineFromLineNumber(line);