DafnyExtension: Added experimental support for diagnosing timeouts.

1 files changed, 17 insertions, 0 deletions

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;