From 8ebe3f941d07ec4a0700fbb616ae390a4e7a2e67 Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Sun, 28 Jul 2013 17:59:29 -0700
Subject: DafnyExtension: Did some refactoring to integrate the Dafny menu more
 tightly.

---
 Source/DafnyExtension/MenuProxy.cs | 109 +++++++++++++++++++++++++++++++++++++
 1 file changed, 109 insertions(+)
 create mode 100644 Source/DafnyExtension/MenuProxy.cs

(limited to 'Source/DafnyExtension/MenuProxy.cs')

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);
+        }
+      }
+    }
+  }
+}
-- 
cgit v1.2.3