From 47e3c9e215f1c5f51d35a974fccb5bd612eaa8be Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Mon, 18 May 2015 23:41:08 +0200
Subject: DafnyExtension: Added experimental support for diagnosing timeouts.

---
 Source/DafnyExtension/MenuProxy.cs | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)

(limited to 'Source/DafnyExtension/MenuProxy.cs')

diff --git a/Source/DafnyExtension/MenuProxy.cs b/Source/DafnyExtension/MenuProxy.cs
index 11e1287f..9ddc8344 100644
--- a/Source/DafnyExtension/MenuProxy.cs
+++ b/Source/DafnyExtension/MenuProxy.cs
@@ -67,6 +67,15 @@ namespace DafnyLanguage
       }
     }
 
+    public void DiagnoseTimeouts(IWpfTextView activeTextView)
+    {
+      DafnyLanguage.ProgressTagger tagger;
+      if (activeTextView != null && DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(activeTextView.TextBuffer, out tagger))
+      {
+        tagger.StartVerification(false, true);
+      }
+    }
+
     public bool MenuEnabled(IWpfTextView activeTextView)
     {
       return activeTextView != null && activeTextView.TextBuffer.ContentType.DisplayName == "dafny";
@@ -80,6 +89,14 @@ namespace DafnyLanguage
                     && resolver.Program != null;
     }
 
+    public bool DiagnoseTimeoutsCommandEnabled(IWpfTextView activeTextView)
+    {
+      ResolverTagger resolver;
+      return activeTextView != null
+                    && DafnyLanguage.ResolverTagger.ResolverTaggers.TryGetValue(activeTextView.TextBuffer, out resolver)
+                    && resolver.VerificationErrors.Any(err => err.Message.Contains("timed out"));
+    }
+
     public void Compile(IWpfTextView activeTextView)
     {
       ResolverTagger resolver;
-- 
cgit v1.2.3