diff options
| -rw-r--r-- | Source/DafnyExtension/DafnyDriver.cs | 6 | ||||
| -rw-r--r-- | Source/DafnyExtension/ProgressMargin.cs | 4 | ||||
| -rw-r--r-- | 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<string, ITextSnapshot> RequestIdToSnapshot = new ConcurrentDictionary<string, ITextSnapshot>();
+ public static readonly ConcurrentDictionary<string, ITextSnapshot> RequestIdToSnapshot = new ConcurrentDictionary<string, ITextSnapshot>();
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 /// </summary>
public sealed class ResolverTagger : ITagger<DafnyResolverTag>, 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<DafnyError> _resolutionErrors = new List<DafnyError>(); // if nonempty, then _snapshot is the snapshot from which the errors were produced
+
List<DafnyError> _verificationErrors = new List<DafnyError>();
- ErrorListProvider _errorProvider;
+ public List<DafnyError> VerificationErrors
+ {
+ get
+ {
+ return _verificationErrors;
+ }
+ set
+ {
+ Contract.Requires(value != null);
- public static IDictionary<string, Dafny.Program> Programs = new ConcurrentDictionary<string, Dafny.Program>();
+ _verificationErrors = value;
+ }
+ }
+
+ public IEnumerable<DafnyError> AllErrors
+ {
+ get
+ {
+ lock (this)
+ {
+ if (_resolutionErrors != null && _resolutionErrors.Any())
+ {
+ return _resolutionErrors;
+ }
+ else
+ {
+ return VerificationErrors;
+ }
+ }
+ }
+ }
+
+ public static readonly IDictionary<string, Dafny.Program> Programs = new ConcurrentDictionary<string, Dafny.Program>();
internal ResolverTagger(ITextBuffer buffer, IServiceProvider serviceProvider, ITextDocumentFactoryService textDocumentFactory) {
_buffer = buffer;
@@ -121,26 +151,13 @@ namespace DafnyLanguage }
}
- public IEnumerable<DafnyError> 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;
- }
- }
-
/// <summary>
/// Find the Error tokens in the set of all tokens and create an ErrorTag for each
/// </summary>
public IEnumerable<ITagSpan<DafnyResolverTag>> 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 : "<program>");
List<DafnyError> newErrors;
@@ -210,21 +226,14 @@ namespace DafnyLanguage Programs.Remove(_document.FilePath);
}
- PopulateErrorList(newErrors, false, snapshot);
+ _resolutionErrors = newErrors;
+ UpdateErrorList(snapshot);
}
- public void PopulateErrorList(List<DafnyError> 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);
|