diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-08-17 11:29:05 -0700 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-08-17 11:29:05 -0700 |
| commit | eaa507dad5904016694a0b019d1e2b8c6406c1c7 (patch) | |
| tree | 791be8464f713064af7883d6c10f5f302ec9ef76 /Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs | |
| parent | 4c5d48ffa0b0e4328ef333d62d7df51190f17f36 (diff) | |
DafnyExtension: toward some fixes
Diffstat (limited to 'Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs')
| -rw-r--r-- | Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs | 28 |
1 files changed, 18 insertions, 10 deletions
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs index e51e9887..a47cdba7 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs +++ b/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs @@ -91,16 +91,24 @@ namespace DafnyLanguage void _aggregator_TagsChanged(object sender, TagsChangedEventArgs e) {
var r = sender as ResolverTagger;
- if (r != null && r._program != null) {
- if (!ComputeOutliningRegions(r._program, r._snapshot))
- return; // no new regions
-
- var chng = TagsChanged;
- if (chng != null) {
- NormalizedSnapshotSpanCollection spans = e.Span.GetSpans(_buffer.CurrentSnapshot);
- if (spans.Count > 0) {
- SnapshotSpan span = new SnapshotSpan(spans[0].Start, spans[spans.Count - 1].End);
- chng(this, new SnapshotSpanEventArgs(span));
+ if (r != null) {
+ ITextSnapshot snap;
+ Microsoft.Dafny.Program prog;
+ lock (this) {
+ snap = r._snapshot;
+ prog = r._program;
+ }
+ if (prog != null) {
+ if (!ComputeOutliningRegions(prog, snap))
+ return; // no new regions
+
+ var chng = TagsChanged;
+ if (chng != null) {
+ NormalizedSnapshotSpanCollection spans = e.Span.GetSpans(_buffer.CurrentSnapshot);
+ if (spans.Count > 0) {
+ SnapshotSpan span = new SnapshotSpan(spans[0].Start, spans[spans.Count - 1].End);
+ chng(this, new SnapshotSpanEventArgs(span));
+ }
}
}
}
|