diff options
| author |  wuestholz <unknown> | 2015-10-26 17:36:25 -0500 |
|---|---|---|
| committer | wuestholz <unknown> | 2015-10-26 17:36:25 -0500 |
| commit | 5e4bcf8e63a3351dc3f0f9bc6cbff8176adddd8b (patch) | |
| tree | b68f21a15903606993f46a12e83343e9eae9c0e5 /Source/DafnyExtension/MenuProxy.cs | |
| parent | b35216f55d22123ae4c35eacf28e99a2b6dbbfaf (diff) | |
DafnyExtension: Add menu item for automatic induction (mainly developed by Rustan).
Diffstat (limited to 'Source/DafnyExtension/MenuProxy.cs')
| -rw-r--r-- | Source/DafnyExtension/MenuProxy.cs | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/Source/DafnyExtension/MenuProxy.cs b/Source/DafnyExtension/MenuProxy.cs index 9ddc8344..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;
|