diff options
| author |  wuestholz <unknown> | 2013-06-07 18:53:40 -0700 |
|---|---|---|
| committer | wuestholz <unknown> | 2013-06-07 18:53:40 -0700 |
| commit | 5b726294d6604001ec162edb4e95d17c0f32b5eb (patch) | |
| tree | 1f1a4a4c99a2d3c6c1484660f93fa5392f202039 /Source/DafnyExtension/ProgressMargin.cs | |
| parent | 1ee9754513e8b4acc885384676df173af5fc0e42 (diff) | |
DafnyExtension: Worked on integrating the verification result caching.
Diffstat (limited to 'Source/DafnyExtension/ProgressMargin.cs')
| -rw-r--r-- | Source/DafnyExtension/ProgressMargin.cs | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/Source/DafnyExtension/ProgressMargin.cs b/Source/DafnyExtension/ProgressMargin.cs index 0a83bcc0..4eb150f5 100644 --- a/Source/DafnyExtension/ProgressMargin.cs +++ b/Source/DafnyExtension/ProgressMargin.cs @@ -273,10 +273,16 @@ namespace DafnyLanguage // Run the verifier
var newErrors = new List<DafnyError>();
try {
- bool success = DafnyDriver.Verify(program, errorInfo => {
- newErrors.Add(new DafnyError(errorInfo.Tok.line - 1, errorInfo.Tok.col - 1, ErrorCategory.VerificationError, errorInfo.Msg));
+ bool success = DafnyDriver.Verify(program, snapshot, errorInfo =>
+ {
+ ITextSnapshot ss = null;
+ if (errorInfo.RequestId != null)
+ {
+ ss = DafnyDriver.RequestIdToSnapshot[errorInfo.RequestId];
+ }
+ newErrors.Add(new DafnyError(errorInfo.Tok.line - 1, errorInfo.Tok.col - 1, ErrorCategory.VerificationError, errorInfo.Msg, ss));
foreach (var aux in errorInfo.Aux) {
- newErrors.Add(new DafnyError(aux.Tok.line - 1, aux.Tok.col - 1, ErrorCategory.AuxInformation, aux.Msg));
+ newErrors.Add(new DafnyError(aux.Tok.line - 1, aux.Tok.col - 1, ErrorCategory.AuxInformation, aux.Msg, ss));
}
});
if (!success) {
|