diff options
| author |  leino <unknown> | 2015-10-26 16:40:55 -0700 |
|---|---|---|
| committer | leino <unknown> | 2015-10-26 16:40:55 -0700 |
| commit | ab999651fc184fdc6a0cb4b52d1253e6c4b9a060 (patch) | |
| tree | 4e715c481755fec2f9e2a1b9c9264cf6f79dbb42 /Source/DafnyExtension | |
| parent | 1dc2166ec1b1de5a19e0de3100eb82527c531b08 (diff) | |
| parent | 5e4bcf8e63a3351dc3f0f9bc6cbff8176adddd8b (diff) | |
Merge
Diffstat (limited to 'Source/DafnyExtension')
| -rw-r--r-- | Source/DafnyExtension/DafnyDriver.cs | 7 | ||||
| -rw-r--r-- | Source/DafnyExtension/MenuProxy.cs | 8 |
2 files changed, 15 insertions, 0 deletions
diff --git a/Source/DafnyExtension/DafnyDriver.cs b/Source/DafnyExtension/DafnyDriver.cs index 2ad05e85..27471d56 100644 --- a/Source/DafnyExtension/DafnyDriver.cs +++ b/Source/DafnyExtension/DafnyDriver.cs @@ -251,6 +251,13 @@ namespace DafnyLanguage return Dafny.DafnyOptions.Clo.VerifySnapshots;
}
+ public static bool ChangeAutomaticInduction() {
+ var old = Dafny.DafnyOptions.O.Induction;
+ // toggle between modes 1 and 3
+ Dafny.DafnyOptions.O.Induction = old == 1 ? 3 : 1;
+ return Dafny.DafnyOptions.O.Induction == 3;
+ }
+
public static bool Verify(Dafny.Program dafnyProgram, ResolverTagger resolver, string uniqueIdPrefix, string requestId, ErrorReporterDelegate er) {
Dafny.Translator translator = new Dafny.Translator(dafnyProgram.reporter);
translator.InsertChecksums = true;
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;
|