diff options
Diffstat (limited to 'Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs')
| -rw-r--r-- | Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs | 264 |
1 files changed, 264 insertions, 0 deletions
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs new file mode 100644 index 00000000..ab2bc790 --- /dev/null +++ b/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs @@ -0,0 +1,264 @@ +//***************************************************************************
+// Copyright © 2010 Microsoft Corporation. All Rights Reserved.
+// 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.Linq;
+using System.Text;
+using System.ComponentModel.Composition;
+using System.Windows.Threading;
+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.Utilities;
+using System.Diagnostics.Contracts;
+using Bpl = Microsoft.Boogie;
+using Dafny = Microsoft.Dafny;
+
+namespace DafnyLanguage
+{
+ [Export(typeof(ITaggerProvider))]
+ [ContentType("dafny")]
+ [TagType(typeof(DafnyTokenTag))]
+ internal sealed class IdentifierTaggerProvider : ITaggerProvider
+ {
+ [Import]
+ internal IBufferTagAggregatorFactoryService AggregatorFactory = 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 IdentifierTagger(buffer, tagAggregator) as ITagger<T>; };
+ return buffer.Properties.GetOrCreateSingletonProperty<ITagger<T>>(sc);
+ }
+ }
+
+ /// <summary>
+ /// Translate DafnyResolverTag's into IOutliningRegionTag's
+ /// </summary>
+ internal sealed class IdentifierTagger : ITagger<DafnyTokenTag>
+ {
+ ITextBuffer _buffer;
+ ITextSnapshot _snapshot; // the most recent snapshot of _buffer that we have been informed about
+ Dafny.Program _program; // the program parsed from _snapshot
+ List<IdRegion> _regions = new List<IdRegion>(); // the regions generated from _program
+ ITagAggregator<DafnyResolverTag> _aggregator;
+
+ internal IdentifierTagger(ITextBuffer buffer, ITagAggregator<DafnyResolverTag> tagAggregator) {
+ _buffer = buffer;
+ _snapshot = _buffer.CurrentSnapshot;
+ _aggregator = tagAggregator;
+ _aggregator.TagsChanged += new EventHandler<TagsChangedEventArgs>(_aggregator_TagsChanged);
+ }
+
+ /// <summary>
+ /// Find the Error tokens in the set of all tokens and create an ErrorTag for each
+ /// </summary>
+ public IEnumerable<ITagSpan<DafnyTokenTag>> GetTags(NormalizedSnapshotSpanCollection spans) {
+ if (spans.Count == 0) yield break;
+ // (A NormalizedSnapshotSpanCollection contains spans that all come from the same snapshot.)
+ // The spans are ordered by the .Start component, and the collection contains no adjacent or abutting spans.
+ // Hence, to find a span that includes all the ones in "spans", we only need to look at the .Start for the
+ // first spand and the .End of the last span:
+ var startPoint = spans[0].Start;
+ var endPoint = spans[spans.Count - 1].End;
+
+ // Note, (startPoint,endPoint) are points in the spans for which we're being asked to provide tags. We need to translate
+ // these back into the most recent snapshot that we've computed regions for, namely _snapshot.
+ var entire = new SnapshotSpan(startPoint, endPoint).TranslateTo(_snapshot, SpanTrackingMode.EdgeExclusive);
+ int start = entire.Start;
+ int end = entire.End;
+ foreach (var r in _regions) {
+ if (0 <= r.Length && r.Start <= end && start <= r.Start + r.Length) {
+ yield return new TagSpan<DafnyTokenTag>(
+ new SnapshotSpan(_snapshot, r.Start, r.Length),
+ new DafnyTokenTag(r.IsDefinition ? DafnyTokenKinds.VariableIdentifierDefinition : DafnyTokenKinds.VariableIdentifier, r.HoverText));
+ }
+ }
+ }
+
+ // the Classifier tagger is translating buffer change events into TagsChanged events, so we don't have to
+ public event EventHandler<SnapshotSpanEventArgs> TagsChanged;
+
+ void _aggregator_TagsChanged(object sender, TagsChangedEventArgs e) {
+ var r = sender as ResolverTagger;
+ if (r != null && r._program != null) {
+ if (!ComputeIdentifierRegions(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));
+ }
+ }
+ }
+ }
+
+ bool ComputeIdentifierRegions(Dafny.Program program, ITextSnapshot snapshot) {
+ Contract.Requires(snapshot != null);
+
+ if (program == _program)
+ return false; // no new regions
+
+ List<IdRegion> newRegions = new List<IdRegion>();
+
+ foreach (var module in program.Modules) {
+ foreach (Dafny.TopLevelDecl d in module.TopLevelDecls) {
+ if (!HasBodyTokens(d) && !(d is Dafny.ClassDecl)) {
+ continue;
+ }
+ if (d is Dafny.DatatypeDecl) {
+ var dt = (Dafny.DatatypeDecl)d;
+ foreach (var ctor in dt.Ctors) {
+ foreach (var dtor in ctor.Destructors) {
+ if (dtor != null) {
+ newRegions.Add(new IdRegion(dtor.tok, dtor, "destructor", true));
+ }
+ }
+ }
+ } else if (d is Dafny.ClassDecl) {
+ var cl = (Dafny.ClassDecl)d;
+ foreach (var member in cl.Members) {
+ if (!HasBodyTokens(member)) {
+ continue;
+ }
+ if (member is Dafny.Function) {
+ var f = (Dafny.Function)member;
+ foreach (var p in f.Formals) {
+ newRegions.Add(new IdRegion(p.tok, p, true));
+ }
+ f.Req.ForEach(e => ExprRegions(e, newRegions));
+ f.Reads.ForEach(e => ExprRegions(e.E, newRegions));
+ f.Ens.ForEach(e => ExprRegions(e, newRegions));
+ f.Decreases.Expressions.ForEach(e => ExprRegions(e, newRegions));
+ if (f.Body != null) {
+ ExprRegions(f.Body, newRegions);
+ }
+ } else if (member is Dafny.Method) {
+ var m = (Dafny.Method)member;
+ foreach (var p in m.Ins) {
+ newRegions.Add(new IdRegion(p.tok, p, true));
+ }
+ foreach (var p in m.Outs) {
+ newRegions.Add(new IdRegion(p.tok, p, true));
+ }
+ m.Req.ForEach(e => ExprRegions(e.E, newRegions));
+ m.Mod.Expressions.ForEach(e => ExprRegions(e.E, newRegions));
+ m.Ens.ForEach(e => ExprRegions(e.E, newRegions));
+ m.Decreases.Expressions.ForEach(e => ExprRegions(e, newRegions));
+ if (m.Body != null) {
+ StatementRegions(m.Body, newRegions);
+ }
+ } else if (member is Dafny.Field) {
+ var fld = (Dafny.Field)member;
+ newRegions.Add(new IdRegion(fld.tok, fld, "field", true));
+ }
+ }
+ }
+ }
+ }
+ _snapshot = snapshot;
+ _regions = newRegions;
+ _program = program;
+ return true;
+ }
+
+ static void ExprRegions(Dafny.Expression expr, List<IdRegion> regions) {
+ Contract.Requires(expr != null);
+ Contract.Requires(regions != null);
+ if (expr is Dafny.IdentifierExpr) {
+ var e = (Dafny.IdentifierExpr)expr;
+ regions.Add(new IdRegion(e.tok, e.Var, false));
+ } else if (expr is Dafny.FieldSelectExpr) {
+ var e = (Dafny.FieldSelectExpr)expr;
+ regions.Add(new IdRegion(e.tok, e.Field, "field", false));
+ } else if (expr is Dafny.ComprehensionExpr) {
+ var e = (Dafny.ComprehensionExpr)expr;
+ foreach (var bv in e.BoundVars) {
+ regions.Add(new IdRegion(bv.tok, bv, true));
+ }
+ } else if (expr is Dafny.MatchExpr) {
+ var e = (Dafny.MatchExpr)expr;
+ foreach (var kase in e.Cases) {
+ kase.Arguments.ForEach(bv => regions.Add(new IdRegion(bv.tok, bv, true)));
+ }
+ }
+ foreach (var ee in expr.SubExpressions) {
+ ExprRegions(ee, regions);
+ }
+ }
+
+ static void StatementRegions(Dafny.Statement stmt, List<IdRegion> regions) {
+ Contract.Requires(stmt != null);
+ Contract.Requires(regions != null);
+ if (stmt is Dafny.VarDecl) {
+ var s = (Dafny.VarDecl)stmt;
+ regions.Add(new IdRegion(s.Tok, s, true));
+ } else if (stmt is Dafny.ParallelStmt) {
+ var s = (Dafny.ParallelStmt)stmt;
+ s.BoundVars.ForEach(bv => regions.Add(new IdRegion(bv.tok, bv, true)));
+ } else if (stmt is Dafny.MatchStmt) {
+ var s = (Dafny.MatchStmt)stmt;
+ foreach (var kase in s.Cases) {
+ kase.Arguments.ForEach(bv => regions.Add(new IdRegion(bv.tok, bv, true)));
+ }
+ }
+ foreach (var ee in stmt.SubExpressions) {
+ ExprRegions(ee, regions);
+ }
+ foreach (var ss in stmt.SubStatements) {
+ StatementRegions(ss, regions);
+ }
+ }
+
+ bool HasBodyTokens(Dafny.Declaration decl) {
+ Contract.Requires(decl != null);
+ return decl.BodyStartTok != Bpl.Token.NoToken && decl.BodyEndTok != Bpl.Token.NoToken;
+ }
+
+ class IdRegion
+ {
+ public readonly int Start;
+ public readonly int Length;
+ public readonly string HoverText;
+ public readonly bool IsDefinition;
+ public IdRegion(Bpl.IToken tok, Dafny.IVariable v, bool isDefinition) {
+ Contract.Requires(tok != null);
+ Contract.Requires(v != null);
+ Start = tok.pos;
+ Length = v.Name.Length;
+ string kind;
+ if (v is Dafny.VarDecl) {
+ kind = "local variable";
+ } else if (v is Dafny.BoundVar) {
+ kind = "bound variable";
+ } else {
+ var formal = (Dafny.Formal)v;
+ kind = formal.InParam ? "in-parameter" : "out-parameter";
+ }
+ HoverText = string.Format("({2}{3}) {0}: {1}", v.Name, v.Type.ToString(), v.IsGhost ? "ghost " : "", kind);
+ IsDefinition = isDefinition;
+ }
+ public IdRegion(Bpl.IToken tok, Dafny.Field decl, string kind, bool isDefinition) {
+ Contract.Requires(tok != null);
+ Contract.Requires(decl != null);
+ Contract.Requires(kind != null);
+ Start = tok.pos;
+ Length = decl.Name.Length;
+ HoverText = string.Format("({2}{3}) {0}: {1}", decl.FullName, decl.Type.ToString(), decl.IsGhost ? "ghost " : "", kind);
+ IsDefinition = isDefinition;
+ }
+ }
+ }
+
+}
|