From e2508e12bf24a84f731884fcbd8f5f128dbf9f9a Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Tue, 11 Jun 2013 09:19:53 -0700
Subject: DafnyExtension: Did some refactoring.

---
 Source/DafnyExtension/DafnyDriver.cs    | 15 ++++-----------
 Source/DafnyExtension/ProgressMargin.cs | 23 +++++++++++++++++------
 2 files changed, 21 insertions(+), 17 deletions(-)

diff --git a/Source/DafnyExtension/DafnyDriver.cs b/Source/DafnyExtension/DafnyDriver.cs
index c9ad6609..4c0ae4fc 100644
--- a/Source/DafnyExtension/DafnyDriver.cs
+++ b/Source/DafnyExtension/DafnyDriver.cs
@@ -148,14 +148,12 @@ namespace DafnyLanguage
 
     #region Boogie interaction
 
-    public static readonly ConcurrentDictionary<string, ITextSnapshot> RequestIdToSnapshot = new ConcurrentDictionary<string, ITextSnapshot>();
-
-    public static bool Verify(Dafny.Program dafnyProgram, ITextSnapshot snapshot, ErrorReporterDelegate er) {
+    public static bool Verify(Dafny.Program dafnyProgram, ITextSnapshot snapshot, string requestId, ErrorReporterDelegate er) {
       Dafny.Translator translator = new Dafny.Translator();
       translator.InsertChecksums = true;
       Bpl.Program boogieProgram = translator.Translate(dafnyProgram);
 
-      PipelineOutcome oc = BoogiePipeline(boogieProgram, snapshot, er);
+      PipelineOutcome oc = BoogiePipeline(boogieProgram, snapshot, requestId, er);
       switch (oc) {
         case PipelineOutcome.Done:
         case PipelineOutcome.VerificationCompleted:
@@ -173,7 +171,8 @@ namespace DafnyLanguage
     /// else.  Hence, any resolution errors and type checking errors are due to errors in
     /// the translation.
     /// </summary>
-    static PipelineOutcome BoogiePipeline(Bpl.Program/*!*/ program, ITextSnapshot snapshot, ErrorReporterDelegate er) {
+    static PipelineOutcome BoogiePipeline(Bpl.Program/*!*/ program, ITextSnapshot snapshot, string requestId, ErrorReporterDelegate er)
+    {
       Contract.Requires(program != null);
 
       PipelineOutcome oc = BoogieResolveAndTypecheck(program);
@@ -181,12 +180,6 @@ namespace DafnyLanguage
         ExecutionEngine.EliminateDeadVariablesAndInline(program);
         ExecutionEngine.errorInformationFactory = new DafnyErrorInformationFactory();
         int errorCount, verified, inconclusives, timeOuts, outOfMemories;
-        string requestId = null;
-        lock (RequestIdToSnapshot)
-        {
-          requestId = (RequestIdToSnapshot.Count + 1).ToString();
-          RequestIdToSnapshot[requestId] = snapshot;
-        }
         return ExecutionEngine.InferAndVerify(program, out errorCount, out verified, out inconclusives, out timeOuts, out outOfMemories, er, requestId);
       }
       return oc;
diff --git a/Source/DafnyExtension/ProgressMargin.cs b/Source/DafnyExtension/ProgressMargin.cs
index 8a8c753b..7a6669ae 100644
--- a/Source/DafnyExtension/ProgressMargin.cs
+++ b/Source/DafnyExtension/ProgressMargin.cs
@@ -171,7 +171,9 @@ namespace DafnyLanguage
     }
 
     public static IDictionary<string, ProgressTagger> ProgressTaggers = new ConcurrentDictionary<string, ProgressTagger>();
-    
+
+    public readonly ConcurrentDictionary<string, ITextSnapshot> RequestIdToSnapshot = new ConcurrentDictionary<string, ITextSnapshot>();
+
     /// <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.
@@ -212,10 +214,18 @@ namespace DafnyLanguage
         var empty = bufferChangesPreVerificationStart;
         bufferChangesPreVerificationStart = bufferChangesPostVerificationStart;
         bufferChangesPostVerificationStart = empty;
+
         // Notify to-whom-it-may-concern about the changes we just made
         NotifyAboutChangedTags(snap);
 
-        verificationWorker = new Thread(() => VerificationWorker(prog, snap, resolver));
+        string requestId = null;
+        lock (RequestIdToSnapshot)
+        {
+          requestId = (RequestIdToSnapshot.Count + 1).ToString();
+          RequestIdToSnapshot[requestId] = snap;
+        }
+
+        verificationWorker = new Thread(() => VerificationWorker(prog, snap, requestId, resolver));
         verificationWorker.IsBackground = true;
         if (_document != null)
         {
@@ -268,21 +278,22 @@ namespace DafnyLanguage
     /// <summary>
     /// Thread entry point.
     /// </summary>
-    void VerificationWorker(Dafny.Program program, ITextSnapshot snapshot, ResolverTagger errorListHolder) {
+    void VerificationWorker(Dafny.Program program, ITextSnapshot snapshot, string requestId, ResolverTagger errorListHolder) {
       Contract.Requires(program != null);
       Contract.Requires(snapshot != null);
+      Contract.Requires(requestId != null);
       Contract.Requires(errorListHolder != null);
 
       // Run the verifier
       var newErrors = new List<DafnyError>();
       try {
-        bool success = DafnyDriver.Verify(program, snapshot, errorInfo =>
+        bool success = DafnyDriver.Verify(program, snapshot, requestId, errorInfo =>
         {
           ITextSnapshot s = snapshot;
           if (errorInfo.RequestId != null)
           {
-            Contract.Assert(DafnyDriver.RequestIdToSnapshot.ContainsKey(errorInfo.RequestId));
-            s = DafnyDriver.RequestIdToSnapshot[errorInfo.RequestId];
+            Contract.Assert(RequestIdToSnapshot.ContainsKey(errorInfo.RequestId));
+            s = RequestIdToSnapshot[errorInfo.RequestId];
           }
           newErrors.Add(new DafnyError(errorInfo.Tok.line - 1, errorInfo.Tok.col - 1, ErrorCategory.VerificationError, errorInfo.Msg, s));
           foreach (var aux in errorInfo.Aux) {
-- 
cgit v1.2.3