diff options
| -rw-r--r-- | Source/Dafny/Resolver.cs | 24 | ||||
| -rw-r--r-- | Util/Emacs/dafny-mode.el | 8 | ||||
| -rw-r--r-- | Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs | 2 |
3 files changed, 18 insertions, 16 deletions
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index 6534d2ba..bf6dce17 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -964,17 +964,19 @@ namespace Microsoft.Dafny allTypeParameters.PopMarker();
}
- foreach (TopLevelDecl d in declarations) {
- if (d is ClassDecl) {
- foreach (var member in ((ClassDecl)d).Members) {
- if (member is Method) {
- var m = ((Method)member);
- if (m.Body != null)
- CheckTypeInference(m.Body);
- } else if (member is Function) {
- var f = (Function)member;
- if (f.Body != null)
- CheckTypeInference(f.Body);
+ if (ErrorCount == prevErrorCount) {
+ foreach (TopLevelDecl d in declarations) {
+ if (d is ClassDecl) {
+ foreach (var member in ((ClassDecl)d).Members) {
+ if (member is Method) {
+ var m = ((Method)member);
+ if (m.Body != null)
+ CheckTypeInference(m.Body);
+ } else if (member is Function) {
+ var f = (Function)member;
+ if (f.Body != null)
+ CheckTypeInference(f.Body);
+ }
}
}
}
diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el index 0b64a775..4f47f9c3 100644 --- a/Util/Emacs/dafny-mode.el +++ b/Util/Emacs/dafny-mode.el @@ -8,7 +8,7 @@ (if dafny-mode-map nil
(setq dafny-mode-map (make-keymap))
- (define-key dafny-mode-map "\C-c\C-c" 'dafny-run-boogie)
+ (define-key dafny-mode-map "\C-c\C-c" 'dafny-run-verifier)
(define-key dafny-mode-map [(control return)] 'font-lock-fontify-buffer))
(setq auto-mode-alist
@@ -69,7 +69,7 @@ dafny-mode-menu (list dafny-mode-map)
"Dafny Mode Menu."
'("Dafny"
- ["Run Boogie" dafny-run-boogie t]
+ ["Run Dafny" dafny-run-verifier t]
"---"
["Recolor buffer" font-lock-fontify-buffer t]
"---"
@@ -81,8 +81,8 @@ (defun dafny-command-line (file)
(concat "boogie " file))
-(defun dafny-run-boogie ()
- "run Boogie to check the Dafny program"
+(defun dafny-run-verifier ()
+ "run Dafny verifier"
(interactive)
(let ((f (buffer-name)))
(compile (dafny-command-line f))))
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs index 86a53460..e51e9887 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs +++ b/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs @@ -78,7 +78,7 @@ namespace DafnyLanguage if (start == end) yield break;
foreach (var r in _regions) {
- if (r.Start <= end && start <= r.Start + r.Length) {
+ if (0 <= r.Length && r.Start <= end && start <= r.Start + r.Length) {
yield return new TagSpan<OutliningRegionTag>(
new SnapshotSpan(_snapshot, r.Start, r.Length),
new OutliningRegionTag(false, false, "...", r.HoverText));
|