diff options
| author |  wuestholz <unknown> | 2013-08-03 18:05:42 -0700 |
|---|---|---|
| committer | wuestholz <unknown> | 2013-08-03 18:05:42 -0700 |
| commit | 04026edf3d0e905362a51995f246d3c2c0807c81 (patch) | |
| tree | 1fa51be1d7095f4f19437e01113b12f5e5027db1 /Source/DafnyExtension/MenuProxy.cs | |
| parent | 8af0f2d97ab5ca1a212c7f4901c43059ccb08e36 (diff) | |
DafnyExtension: Did some refactoring and added a description to error states.
Diffstat (limited to 'Source/DafnyExtension/MenuProxy.cs')
| -rw-r--r-- | Source/DafnyExtension/MenuProxy.cs | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/Source/DafnyExtension/MenuProxy.cs b/Source/DafnyExtension/MenuProxy.cs index fc0c0d1d..59afc448 100644 --- a/Source/DafnyExtension/MenuProxy.cs +++ b/Source/DafnyExtension/MenuProxy.cs @@ -85,7 +85,7 @@ namespace DafnyLanguage return activeTextView != null
&& DafnyLanguage.ResolverTagger.ResolverTaggers.TryGetValue(activeTextView.TextBuffer, out resolver)
&& resolver.Program != null
- && resolver.VerificationErrors.Any(err => !string.IsNullOrEmpty(err.Model));
+ && resolver.VerificationErrors.Any(err => !string.IsNullOrEmpty(err.ModelText));
}
public void ShowErrorModel(IWpfTextView activeTextView)
@@ -94,14 +94,14 @@ namespace DafnyLanguage var show = activeTextView != null
&& DafnyLanguage.ResolverTagger.ResolverTaggers.TryGetValue(activeTextView.TextBuffer, out resolver)
&& resolver.Program != null
- && resolver.VerificationErrors.Any(err => err.IsSelected && !string.IsNullOrEmpty(err.Model));
+ && resolver.VerificationErrors.Any(err => err.IsSelected && !string.IsNullOrEmpty(err.ModelText));
if (show)
{
- var selectedError = resolver.VerificationErrors.FirstOrDefault(err => err.IsSelected && !string.IsNullOrEmpty(err.Model));
+ var selectedError = resolver.VerificationErrors.FirstOrDefault(err => err.IsSelected && !string.IsNullOrEmpty(err.ModelText));
if (selectedError != null)
{
- DafnyMenuPackage.ShowErrorModelInBVD(selectedError.Model, selectedError.SelectedStateId);
+ DafnyMenuPackage.ShowErrorModelInBVD(selectedError.ModelText, selectedError.SelectedStateId);
}
}
}
|