From 79eb84f316da7d481cc3648d16fe9f0a911edd53 Mon Sep 17 00:00:00 2001 From: wuestholz Date: Mon, 10 Jun 2013 16:28:14 -0700 Subject: DafnyExtension: Did some refactoring. --- Source/DafnyExtension/DafnyDriver.cs | 6 +-- Source/DafnyExtension/ProgressMargin.cs | 4 +- Source/DafnyExtension/ResolverTagger.cs | 87 ++++++++++++++++++--------------- 3 files changed, 53 insertions(+), 44 deletions(-) diff --git a/Source/DafnyExtension/DafnyDriver.cs b/Source/DafnyExtension/DafnyDriver.cs index 21e081b6..c9ad6609 100644 --- a/Source/DafnyExtension/DafnyDriver.cs +++ b/Source/DafnyExtension/DafnyDriver.cs @@ -1,10 +1,8 @@ -using System; -using System.Collections.Concurrent; +using System.Collections.Concurrent; using System.Collections.Generic; using System.Diagnostics.Contracts; using Microsoft.Boogie; using Microsoft.VisualStudio.Text; -using VC; using Bpl = Microsoft.Boogie; using Dafny = Microsoft.Dafny; @@ -150,7 +148,7 @@ namespace DafnyLanguage #region Boogie interaction - public static ConcurrentDictionary RequestIdToSnapshot = new ConcurrentDictionary(); + public static readonly ConcurrentDictionary RequestIdToSnapshot = new ConcurrentDictionary(); public static bool Verify(Dafny.Program dafnyProgram, ITextSnapshot snapshot, ErrorReporterDelegate er) { Dafny.Translator translator = new Dafny.Translator(); diff --git a/Source/DafnyExtension/ProgressMargin.cs b/Source/DafnyExtension/ProgressMargin.cs index d587d3dd..e38d9eea 100644 --- a/Source/DafnyExtension/ProgressMargin.cs +++ b/Source/DafnyExtension/ProgressMargin.cs @@ -292,7 +292,9 @@ namespace DafnyLanguage } catch (Exception e) { newErrors.Add(new DafnyError(0, 0, ErrorCategory.InternalError, "verification process error: " + e.Message, snapshot)); } - errorListHolder.PopulateErrorList(newErrors, true, snapshot); + + errorListHolder.VerificationErrors = newErrors; + errorListHolder.UpdateErrorList(snapshot); lock (this) { bufferChangesPreVerificationStart.Clear(); diff --git a/Source/DafnyExtension/ResolverTagger.cs b/Source/DafnyExtension/ResolverTagger.cs index 07bf33bf..a4d4a690 100644 --- a/Source/DafnyExtension/ResolverTagger.cs +++ b/Source/DafnyExtension/ResolverTagger.cs @@ -3,25 +3,21 @@ // This code released under the terms of the // Microsoft Public License (MS-PL, http://opensource.org/licenses/ms-pl.html.) //*************************************************************************** -using EnvDTE; + using System; -using System.Collections.Generic; -using System.Collections.Concurrent; using System.Linq; -using System.Text; +using System.Collections.Concurrent; +using System.Collections.Generic; using System.ComponentModel.Composition; -using System.Windows.Threading; +using System.Diagnostics.Contracts; +using EnvDTE; using Microsoft.VisualStudio; using Microsoft.VisualStudio.Shell; using Microsoft.VisualStudio.Shell.Interop; using Microsoft.VisualStudio.Text; -using Microsoft.VisualStudio.Text.Classification; -using Microsoft.VisualStudio.Text.Editor; using Microsoft.VisualStudio.Text.Tagging; -using Microsoft.VisualStudio.Text.Projection; using Microsoft.VisualStudio.TextManager.Interop; using Microsoft.VisualStudio.Utilities; -using System.Diagnostics.Contracts; using Dafny = Microsoft.Dafny; namespace DafnyLanguage @@ -69,16 +65,50 @@ namespace DafnyLanguage /// public sealed class ResolverTagger : ITagger, IDisposable { - ITextBuffer _buffer; - ITextDocument _document; + readonly ITextBuffer _buffer; + readonly ITextDocument _document; + readonly ErrorListProvider _errorProvider; + // The _snapshot and _program fields should be updated and read together, so they are protected by "this" public ITextSnapshot _snapshot; // may be null public Dafny.Program _program; // non-null only if the snapshot contains a Dafny program that type checks + List _resolutionErrors = new List(); // if nonempty, then _snapshot is the snapshot from which the errors were produced + List _verificationErrors = new List(); - ErrorListProvider _errorProvider; + public List VerificationErrors + { + get + { + return _verificationErrors; + } + set + { + Contract.Requires(value != null); - public static IDictionary Programs = new ConcurrentDictionary(); + _verificationErrors = value; + } + } + + public IEnumerable AllErrors + { + get + { + lock (this) + { + if (_resolutionErrors != null && _resolutionErrors.Any()) + { + return _resolutionErrors; + } + else + { + return VerificationErrors; + } + } + } + } + + public static readonly IDictionary Programs = new ConcurrentDictionary(); internal ResolverTagger(ITextBuffer buffer, IServiceProvider serviceProvider, ITextDocumentFactoryService textDocumentFactory) { _buffer = buffer; @@ -121,26 +151,13 @@ namespace DafnyLanguage } } - public IEnumerable AllErrors() { - foreach (var err in _resolutionErrors) { - yield return err; - } - if (_resolutionErrors.Count != 0) { - // we're done - yield break; - } - foreach (var err in _verificationErrors) { - yield return err; - } - } - /// /// Find the Error tokens in the set of all tokens and create an ErrorTag for each /// public IEnumerable> GetTags(NormalizedSnapshotSpanCollection spans) { if (spans.Count == 0) yield break; var currentSnapshot = spans[0].Snapshot; - foreach (var err in AllErrors()) { + foreach (var err in AllErrors) { if (err.Category != ErrorCategory.ProcessError) { var span = err.Span.TranslateTo(currentSnapshot, SpanTrackingMode.EdgeExclusive); string ty; // the COLORs below indicate what I see on my machine @@ -183,7 +200,6 @@ namespace DafnyLanguage ITextSnapshot snapshot = _buffer.CurrentSnapshot; if (snapshot == _snapshot) return; // we've already done this snapshot - NormalizedSnapshotSpanCollection spans = new NormalizedSnapshotSpanCollection(new SnapshotSpan(snapshot, 0, snapshot.Length)); var driver = new DafnyDriver(snapshot, _document != null ? _document.FilePath : ""); List newErrors; @@ -210,21 +226,14 @@ namespace DafnyLanguage Programs.Remove(_document.FilePath); } - PopulateErrorList(newErrors, false, snapshot); + _resolutionErrors = newErrors; + UpdateErrorList(snapshot); } - public void PopulateErrorList(List newErrors, bool verificationErrors, ITextSnapshot snapshot) { - Contract.Requires(newErrors != null); - - if (verificationErrors) { - _verificationErrors = newErrors; - } else { - _resolutionErrors = newErrors; - } - + public void UpdateErrorList(ITextSnapshot snapshot) { _errorProvider.SuspendRefresh(); // reduce flickering _errorProvider.Tasks.Clear(); - foreach (var err in AllErrors()) { + foreach (var err in AllErrors) { var span = err.Span.TranslateTo(snapshot, SpanTrackingMode.EdgeExclusive); var lineNum = snapshot.GetLineNumberFromPosition(span.Start.Position); var line = snapshot.GetLineFromPosition(span.Start.Position); -- cgit v1.2.3