summaryrefslogtreecommitdiff
path: root/Source/DafnyExtension/DafnyDriver.cs
diff options
context:
space:
mode:
authorGravatar wuestholz <unknown>2013-06-18 20:20:18 -0700
committerGravatar wuestholz <unknown>2013-06-18 20:20:18 -0700
commitf8b97acc643165b1ad986894398512946605de7b (patch)
tree1a0e8a23339eccf492d7bcf1a0907c5c79b571f9 /Source/DafnyExtension/DafnyDriver.cs
parent6df8bbdb3fc417de28a0b386590b2a1860d6472a (diff)
Did some refactoring of the error reporting functionality.
Diffstat (limited to 'Source/DafnyExtension/DafnyDriver.cs')
-rw-r--r--Source/DafnyExtension/DafnyDriver.cs4
1 files changed, 4 insertions, 0 deletions
diff --git a/Source/DafnyExtension/DafnyDriver.cs b/Source/DafnyExtension/DafnyDriver.cs
index d795451c..27c471b2 100644
--- a/Source/DafnyExtension/DafnyDriver.cs
+++ b/Source/DafnyExtension/DafnyDriver.cs
@@ -69,6 +69,10 @@ namespace DafnyLanguage
public void WriteTrailer(int verified, int errors, int inconclusives, int timeOuts, int outOfMemories)
{
}
+
+ public void WriteErrorInformation(ErrorInformation errorInfo, bool isError, bool showBplLocation)
+ {
+ }
}
#endregion