diff options
| author |  wuestholz <unknown> | 2013-07-28 17:59:29 -0700 |
|---|---|---|
| committer | wuestholz <unknown> | 2013-07-28 17:59:29 -0700 |
| commit | 8ebe3f941d07ec4a0700fbb616ae390a4e7a2e67 (patch) | |
| tree | 299684da321cdf59df09f8941abc180ab642c906 /Source/DafnyExtension/MenuProxy.cs | |
| parent | 9138e7c13a7161b6431857c6b29157cdcaa26821 (diff) | |
DafnyExtension: Did some refactoring to integrate the Dafny menu more tightly.
Diffstat (limited to 'Source/DafnyExtension/MenuProxy.cs')
| -rw-r--r-- | Source/DafnyExtension/MenuProxy.cs | 109 |
1 files changed, 109 insertions, 0 deletions
diff --git a/Source/DafnyExtension/MenuProxy.cs b/Source/DafnyExtension/MenuProxy.cs new file mode 100644 index 00000000..69bf03d3 --- /dev/null +++ b/Source/DafnyExtension/MenuProxy.cs @@ -0,0 +1,109 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Threading.Tasks;
+using Microsoft.VisualStudio.Text.Editor;
+
+namespace DafnyLanguage
+{
+ class MenuProxy : DafnyLanguage.DafnyMenu.IMenuProxy
+ {
+ private DafnyMenu.DafnyMenuPackage DafnyMenuPackage;
+
+ public MenuProxy(DafnyMenu.DafnyMenuPackage DafnyMenuPackage)
+ {
+ this.DafnyMenuPackage = DafnyMenuPackage;
+ }
+
+ public bool ToggleSnapshotVerification(IWpfTextView activeTextView)
+ {
+ return DafnyDriver.ToggleIncrementalVerification();
+ }
+
+ public bool StopVerifierCommandEnabled(IWpfTextView activeTextView)
+ {
+ DafnyLanguage.ProgressTagger tagger;
+ return activeTextView != null
+ && DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(activeTextView.TextBuffer, out tagger)
+ && tagger != null && tagger.VerificationDisabled;
+ }
+
+ public void StopVerifier(IWpfTextView activeTextView)
+ {
+ DafnyLanguage.ProgressTagger tagger;
+ if (activeTextView != null && DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(activeTextView.TextBuffer, out tagger))
+ {
+ tagger.StopVerification();
+ }
+ }
+
+ public bool RunVerifierCommandEnabled(IWpfTextView activeTextView)
+ {
+ DafnyLanguage.ProgressTagger tagger;
+ return activeTextView != null
+ && DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(activeTextView.TextBuffer, out tagger)
+ && tagger != null && tagger.VerificationDisabled;
+ }
+
+ public void RunVerifier(IWpfTextView activeTextView)
+ {
+ DafnyLanguage.ProgressTagger tagger;
+ if (activeTextView != null && DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(activeTextView.TextBuffer, out tagger))
+ {
+ tagger.StartVerification();
+ }
+ }
+
+ public bool MenuEnabled(IWpfTextView activeTextView)
+ {
+ return activeTextView != null && activeTextView.TextBuffer.ContentType.DisplayName == "dafny";
+ }
+
+ public bool CompileCommandEnabled(IWpfTextView activeTextView)
+ {
+ ResolverTagger resolver;
+ return activeTextView != null
+ && DafnyLanguage.ResolverTagger.ResolverTaggers.TryGetValue(activeTextView.TextBuffer, out resolver)
+ && resolver.Program != null;
+ }
+
+ public void Compile(IWpfTextView activeTextView)
+ {
+ ResolverTagger resolver;
+ if (activeTextView != null
+ && DafnyLanguage.ResolverTagger.ResolverTaggers.TryGetValue(activeTextView.TextBuffer, out resolver)
+ && resolver.Program != null)
+ {
+ DafnyMenuPackage.ExecuteAsCompiling(() => { DafnyDriver.Compile(resolver.Program); });
+ }
+ }
+
+ public bool ShowErrorModelCommandEnabled(IWpfTextView activeTextView)
+ {
+ ResolverTagger resolver;
+ return activeTextView != null
+ && DafnyLanguage.ResolverTagger.ResolverTaggers.TryGetValue(activeTextView.TextBuffer, out resolver)
+ && resolver.Program != null
+ && resolver.VerificationErrors.Any(err => !string.IsNullOrEmpty(err.Model));
+ }
+
+ public void ShowErrorModel(IWpfTextView activeTextView)
+ {
+ ResolverTagger resolver = null;
+ var show = activeTextView != null
+ && DafnyLanguage.ResolverTagger.ResolverTaggers.TryGetValue(activeTextView.TextBuffer, out resolver)
+ && resolver.Program != null
+ && resolver.VerificationErrors.Any(err => err.IsSelected && !string.IsNullOrEmpty(err.Model));
+ if (show)
+ {
+ var selectedError = resolver.VerificationErrors.FirstOrDefault(err => err.IsSelected && !string.IsNullOrEmpty(err.Model));
+
+ if (selectedError != null)
+ {
+ DafnyMenuPackage.ShowErrorModel(selectedError.Model, selectedError.SelectedStateId);
+ }
+ }
+ }
+ }
+}
|