DafnyExtension: Added a button to the menu for stopping/starting the verifier.

6 files changed, 150 insertions, 19 deletions

diff --git a/Source/DafnyExtension/DafnyExtension.csproj b/Source/DafnyExtension/DafnyExtension.csproj
index 9399a1d2..844699ee 100644
--- a/Source/DafnyExtension/DafnyExtension.csproj
+++ b/Source/DafnyExtension/DafnyExtension.csproj
@@ -1,4 +1,4 @@
-<?xml version="1.0" encoding="utf-8"?>

+<?xml version="1.0" encoding="utf-8"?>

 <Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">

   <Import Project="$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props" Condition="Exists('$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props')" />

   <PropertyGroup>

@@ -228,4 +228,4 @@ copy /y $(SolutionDir)\..\Binaries\DafnyRuntime.cs $(ProjectDir)</PreBuildEvent>
   <Target Name="AfterBuild">

   </Target>

   -->

-</Project>

+</Project>
\ No newline at end of file
diff --git a/Source/DafnyExtension/ProgressMargin.cs b/Source/DafnyExtension/ProgressMargin.cs
index 3f4da8ed..edaa5019 100644
--- a/Source/DafnyExtension/ProgressMargin.cs
+++ b/Source/DafnyExtension/ProgressMargin.cs
@@ -1,5 +1,6 @@
 using System;

 using System.Collections.Generic;

+using System.Collections.Concurrent;

 using System.Threading;

 using System.Windows.Threading;

 using System.Windows;

@@ -71,23 +72,33 @@ namespace DafnyLanguage
     [Import(typeof(Microsoft.VisualStudio.Shell.SVsServiceProvider))]

     internal IServiceProvider _serviceProvider = null;

 

+    [Import]

+    ITextDocumentFactoryService _textDocumentFactory = null;

+

     public ITagger<T> CreateTagger<T>(ITextBuffer buffer) where T : ITag {

       ITagAggregator<DafnyResolverTag> tagAggregator = AggregatorFactory.CreateTagAggregator<DafnyResolverTag>(buffer);

       // create a single tagger for each buffer.

-      Func<ITagger<T>> sc = delegate() { return new ProgressTagger(buffer, _serviceProvider, tagAggregator) as ITagger<T>; };

+      Func<ITagger<T>> sc = delegate() { return new ProgressTagger(buffer, _serviceProvider, tagAggregator, _textDocumentFactory) as ITagger<T>; };

       return buffer.Properties.GetOrCreateSingletonProperty<ITagger<T>>(sc);

     }

   }

 

-  internal class ProgressTagger : ITagger<ProgressGlyphTag>, IDisposable

+  public class ProgressTagger : ITagger<ProgressGlyphTag>, IDisposable

   {

     ErrorListProvider _errorProvider;

     ITextBuffer _buffer;

+    ITextDocument _document;

 

     readonly DispatcherTimer timer;

 

-    public ProgressTagger(ITextBuffer buffer, IServiceProvider serviceProvider, ITagAggregator<DafnyResolverTag> tagAggregator) {

+    public ProgressTagger(ITextBuffer buffer, IServiceProvider serviceProvider, ITagAggregator<DafnyResolverTag> tagAggregator, ITextDocumentFactoryService textDocumentFactory) {

       _buffer = buffer;

+

+      if (!textDocumentFactory.TryGetTextDocument(_buffer, out _document))

+      {

+        _document = null;

+      }

+

       _errorProvider = new ErrorListProvider(serviceProvider);

 

       timer = new DispatcherTimer(DispatcherPriority.ApplicationIdle);

@@ -132,6 +143,16 @@ namespace DafnyLanguage
     }

 

     bool verificationInProgress;  // this field is protected by "this".  Invariant:  !verificationInProgress ==> bufferChangesPreVerificationStart.Count == 0

+    Thread verificationWorker;

+    bool verificationDisabled;

+

+    public bool VerificationDisabled

+    {

+      get { return verificationDisabled; }

+    }

+

+    public static IDictionary<string, ProgressTagger> ProgressTaggers = new ConcurrentDictionary<string, ProgressTagger>();

+    

     /// <summary>

     /// This method is invoked when the user has been idle for a little while.

     /// Note, "sender" and "args" are allowed to be passed in as null--they are not used by this method.

@@ -139,7 +160,6 @@ namespace DafnyLanguage
     public void UponIdle(object sender, EventArgs args) {

       Dafny.Program prog;

       ITextSnapshot snap;

-      ResolverTagger r;

       lock (this) {

         if (verificationInProgress) {

           // This UponIdle message came at an inopportune time--we've already kicked off a verification.

@@ -152,9 +172,7 @@ namespace DafnyLanguage
           prog = resolver._program;

           snap = resolver._snapshot;

         }

-        r = resolver;

-        resolver = null;

-        if (prog == null) return;

+        if (prog == null || verificationDisabled) return;

         // We have a successfully resolved program to verify

 

         var resolvedVersion = snap.Version.VersionNumber;

@@ -176,15 +194,54 @@ namespace DafnyLanguage
         bufferChangesPreVerificationStart = bufferChangesPostVerificationStart;

         bufferChangesPostVerificationStart = empty;

         // Notify to-whom-it-may-concern about the changes we just made

-        var chng = TagsChanged;

-        if (chng != null) {

-          chng(this, new SnapshotSpanEventArgs(new SnapshotSpan(snap, 0, snap.Length)));

+        NotifyAboutChangedTags(snap);

+

+        verificationWorker = new Thread(() => VerificationWorker(prog, snap, resolver));

+        verificationWorker.IsBackground = true;

+        if (_document != null)

+        {

+          ProgressTaggers[_document.FilePath] = this;

         }

+      }

+      verificationWorker.Start();

+    }

 

+    private void NotifyAboutChangedTags(ITextSnapshot snap)

+    {

+      var chng = TagsChanged;

+      if (chng != null)

+      {

+        chng(this, new SnapshotSpanEventArgs(new SnapshotSpan(snap, 0, snap.Length)));

       }

-      new Thread(() => VerificationWorker(prog, snap, r)).Start();

     }

 

+    public void StopVerification()

+    {

+      verificationWorker.Abort();  // TODO(wuestholz): Make sure this kills the corresponding Z3 process.

+      lock (this)

+      {

+        bufferChangesPreVerificationStart.Clear();

+        bufferChangesPostVerificationStart.Clear();

+        bufferChangesPostVerificationStart.Add(new SnapshotSpan(_buffer.CurrentSnapshot, 0, _buffer.CurrentSnapshot.Length));

+        verificationDisabled = true;

+        verificationInProgress = false;

+        NotifyAboutChangedTags(_buffer.CurrentSnapshot);

+      }

+    }

+

+    public void StartVerification()

+    {

+      lock (this)

+      {

+        bufferChangesPreVerificationStart.Clear();

+        bufferChangesPostVerificationStart.Clear();

+        bufferChangesPostVerificationStart.Add(new SnapshotSpan(_buffer.CurrentSnapshot, 0, _buffer.CurrentSnapshot.Length));

+        verificationDisabled = false;

+        NotifyAboutChangedTags(_buffer.CurrentSnapshot);

+      }

+    }

+

+

     /// <summary>

     /// Thread entry point.

     /// </summary>

@@ -209,16 +266,13 @@ namespace DafnyLanguage
         newErrors.Add(new DafnyError(0, 0, ErrorCategory.InternalError, "verification process error: " + e.Message));

       }

       errorListHolder.PopulateErrorList(newErrors, true, snapshot);

-

+      

       lock (this) {

         bufferChangesPreVerificationStart.Clear();

         verificationInProgress = false;

       }

       // Notify to-whom-it-may-concern about the cleared pre-verification changes

-      var chng = TagsChanged;

-      if (chng != null) {

-        chng(this, new SnapshotSpanEventArgs(new SnapshotSpan(snapshot, 0, snapshot.Length)));

-      }

+      NotifyAboutChangedTags(snapshot);

 

       // If new changes took place since we started the verification, we may need to kick off another verification

       // immediately.

diff --git a/Source/DafnyMenu/DafnyMenu.csproj b/Source/DafnyMenu/DafnyMenu.csproj
index 3df7f083..e3500e26 100644
--- a/Source/DafnyMenu/DafnyMenu.csproj
+++ b/Source/DafnyMenu/DafnyMenu.csproj
@@ -25,10 +25,11 @@
     <DebugSymbols>true</DebugSymbols>

     <DebugType>full</DebugType>

     <Optimize>false</Optimize>

-    <OutputPath>bin\Debug\</OutputPath>

+    <OutputPath>..\..\Binaries\</OutputPath>

     <DefineConstants>DEBUG;TRACE</DefineConstants>

     <ErrorReport>prompt</ErrorReport>

     <WarningLevel>4</WarningLevel>

+    <CopyVsixExtensionFiles>False</CopyVsixExtensionFiles>

   </PropertyGroup>

   <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">

     <DebugType>pdbonly</DebugType>

diff --git a/Source/DafnyMenu/DafnyMenu.vsct b/Source/DafnyMenu/DafnyMenu.vsct
index 1d0c783b..812a06e8 100644
--- a/Source/DafnyMenu/DafnyMenu.vsct
+++ b/Source/DafnyMenu/DafnyMenu.vsct
@@ -77,6 +77,24 @@
         </Strings>

       </Button>

 

+      <Button guid="guidDafnyMenuCmdSet" id="cmdidRunVerifier" priority="0x0101" type="Button">

+        <Parent guid="guidDafnyMenuCmdSet" id="DafnyMenuGroup" />

+        <CommandFlag>DefaultInvisible</CommandFlag>

+        <CommandFlag>DynamicVisibility</CommandFlag>

+        <Strings>

+          <ButtonText>Run verifier</ButtonText>

+        </Strings>

+      </Button>

+

+      <Button guid="guidDafnyMenuCmdSet" id="cmdidStopVerifier" priority="0x0102" type="Button">

+        <Parent guid="guidDafnyMenuCmdSet" id="DafnyMenuGroup" />

+        <CommandFlag>DefaultInvisible</CommandFlag>

+        <CommandFlag>DynamicVisibility</CommandFlag>

+        <Strings>

+          <ButtonText>Stop verifier</ButtonText>

+        </Strings>

+      </Button>

+

     </Buttons>

 

     <!--The bitmaps section is used to define the bitmaps that are used for the commands.-->

@@ -104,6 +122,8 @@
     <GuidSymbol name="guidDafnyMenuCmdSet" value="{393ad46d-e125-41ce-84ee-b4d552d5ba16}">

       <IDSymbol name="DafnyMenuGroup" value="0x1020" />

       <IDSymbol name="cmdidCompile" value="0x0100" />

+      <IDSymbol name="cmdidRunVerifier" value="0x0101" />

+      <IDSymbol name="cmdidStopVerifier" value="0x0102" />

     </GuidSymbol>

 

     <!--

diff --git a/Source/DafnyMenu/DafnyMenuPackage.cs b/Source/DafnyMenu/DafnyMenuPackage.cs
index c0784955..3362f2b3 100644
--- a/Source/DafnyMenu/DafnyMenuPackage.cs
+++ b/Source/DafnyMenu/DafnyMenuPackage.cs
@@ -36,6 +36,8 @@ namespace DafnyLanguage.DafnyMenu
 

     private OleMenuCommand compileCommand;

     private OleMenuCommand menuCommand;

+    private OleMenuCommand runVerifierCommand;

+    private OleMenuCommand stopVerifierCommand;

 

     /// <summary>

     /// Default constructor of the package.

@@ -72,6 +74,18 @@ namespace DafnyLanguage.DafnyMenu
         compileCommand.BeforeQueryStatus += compileCommand_BeforeQueryStatus;

         mcs.AddCommand(compileCommand);

 

+        var runVerifierCommandID = new CommandID(GuidList.guidDafnyMenuCmdSet, (int)PkgCmdIDList.cmdidRunVerifier);

+        runVerifierCommand = new OleMenuCommand(RunVerifierCallback, runVerifierCommandID);

+        runVerifierCommand.Enabled = true;

+        runVerifierCommand.BeforeQueryStatus += runVerifierCommand_BeforeQueryStatus;

+        mcs.AddCommand(runVerifierCommand);

+

+        var stopVerifierCommandID = new CommandID(GuidList.guidDafnyMenuCmdSet, (int)PkgCmdIDList.cmdidStopVerifier);

+        stopVerifierCommand = new OleMenuCommand(StopVerifierCallback, stopVerifierCommandID);

+        stopVerifierCommand.Enabled = true;

+        stopVerifierCommand.BeforeQueryStatus += stopVerifierCommand_BeforeQueryStatus;

+        mcs.AddCommand(stopVerifierCommand);

+

         var menuCommandID = new CommandID(GuidList.guidDafnyMenuPkgSet, (int)PkgCmdIDList.cmdidMenu);

         menuCommand = new OleMenuCommand(new EventHandler((sender, e) => { }), menuCommandID);

         menuCommand.BeforeQueryStatus += menuCommand_BeforeQueryStatus;

@@ -81,6 +95,28 @@ namespace DafnyLanguage.DafnyMenu
       }

     }

 

+    private void StopVerifierCallback(object sender, EventArgs e)

+    {

+      var dte = GetGlobalService(typeof(EnvDTE.DTE)) as EnvDTE.DTE;

+      DafnyLanguage.ProgressTagger tagger;

+      DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(dte.ActiveDocument.FullName, out tagger);

+      if (tagger != null)

+      {

+        tagger.StopVerification();

+      }

+    }

+

+    private void RunVerifierCallback(object sender, EventArgs e)

+    {

+      var dte = GetGlobalService(typeof(EnvDTE.DTE)) as EnvDTE.DTE;

+      DafnyLanguage.ProgressTagger tagger;

+      DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(dte.ActiveDocument.FullName, out tagger);

+      if (tagger != null)

+      {

+        tagger.StartVerification();

+      }

+    }

+

     void menuCommand_BeforeQueryStatus(object sender, EventArgs e)

     {

       var dte = GetGlobalService(typeof(EnvDTE.DTE)) as EnvDTE.DTE;

@@ -89,6 +125,24 @@ namespace DafnyLanguage.DafnyMenu
       menuCommand.Enabled = isActive;

     }

 

+    void runVerifierCommand_BeforeQueryStatus(object sender, EventArgs e)

+    {

+      var dte = GetGlobalService(typeof(EnvDTE.DTE)) as EnvDTE.DTE;

+      DafnyLanguage.ProgressTagger tagger;

+      DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(dte.ActiveDocument.FullName, out tagger);  

+      runVerifierCommand.Visible = tagger != null && tagger.VerificationDisabled;

+      runVerifierCommand.Enabled = tagger != null && tagger.VerificationDisabled;

+    }

+

+    void stopVerifierCommand_BeforeQueryStatus(object sender, EventArgs e)

+    {

+      var dte = GetGlobalService(typeof(EnvDTE.DTE)) as EnvDTE.DTE;

+      DafnyLanguage.ProgressTagger tagger;

+      DafnyLanguage.ProgressTagger.ProgressTaggers.TryGetValue(dte.ActiveDocument.FullName, out tagger);  

+      stopVerifierCommand.Visible = !(tagger != null && tagger.VerificationDisabled);

+      stopVerifierCommand.Enabled = !(tagger != null && tagger.VerificationDisabled);

+    }

+

     void compileCommand_BeforeQueryStatus(object sender, EventArgs e)

     {

       var dte = GetGlobalService(typeof(EnvDTE.DTE)) as EnvDTE.DTE;

diff --git a/Source/DafnyMenu/PkgCmdID.cs b/Source/DafnyMenu/PkgCmdID.cs
index 1b786829..5f0213cc 100644
--- a/Source/DafnyMenu/PkgCmdID.cs
+++ b/Source/DafnyMenu/PkgCmdID.cs
@@ -7,6 +7,8 @@ namespace DafnyLanguage.DafnyMenu
   static class PkgCmdIDList

   {

     public const uint cmdidCompile = 0x100;

+    public const uint cmdidRunVerifier = 0x101;

+    public const uint cmdidStopVerifier = 0x102;

     public const uint cmdidMenu = 0x1021;

   };

 }
\ No newline at end of file