Merge commit 'df5c5f5'

1 files changed, 25 insertions, 0 deletions

diff --git a/Source/DafnyExtension/MenuProxy.cs b/Source/DafnyExtension/MenuProxy.cs
index 11e1287f..0e061cd3 100644
--- a/Source/DafnyExtension/MenuProxy.cs
+++ b/Source/DafnyExtension/MenuProxy.cs
@@ -33,6 +33,14 @@ namespace DafnyLanguage
              && 0 < DafnyDriver.IncrementalVerificationMode();

     }

 

+    public bool ToggleAutomaticInduction(IWpfTextView activeTextView) {

+      return DafnyDriver.ChangeAutomaticInduction();

+    }

+

+    public bool AutomaticInductionCommandEnabled(IWpfTextView activeTextView) {

+      return activeTextView != null;

+    }

+

     public bool StopVerifierCommandEnabled(IWpfTextView activeTextView)

     {

       DafnyLanguage.ProgressTagger tagger;

@@ -67,6 +75,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 +97,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;