From 868ae26aa67deceae8a5878a55156424642d47c3 Mon Sep 17 00:00:00 2001 From: Unknown Date: Wed, 15 Aug 2012 16:07:54 -0700 Subject: Dafny: added Statement.SubExpressions getter DafnyExtension: added hover text for identifiers --- .../DafnyExtension/ClassificationTagger.cs | 12 +- .../DafnyExtension/DafnyExtension.csproj | 2 + .../DafnyExtension/DafnyExtension/HoverText.cs | 134 +++++++++++ .../DafnyExtension/IdentifierTagger.cs | 264 +++++++++++++++++++++ .../DafnyExtension/ResolverTagger.cs | 1 - 5 files changed, 406 insertions(+), 7 deletions(-) create mode 100644 Util/VS2010/DafnyExtension/DafnyExtension/HoverText.cs create mode 100644 Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs (limited to 'Util') diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/ClassificationTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/ClassificationTagger.cs index 7e64dd1d..09835ac9 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/ClassificationTagger.cs +++ b/Util/VS2010/DafnyExtension/DafnyExtension/ClassificationTagger.cs @@ -50,7 +50,7 @@ namespace DafnyLanguage _typeMap[DafnyTokenKinds.String] = standards.StringLiteral; _typeMap[DafnyTokenKinds.Comment] = standards.Comment; _typeMap[DafnyTokenKinds.VariableIdentifier] = standards.Identifier; - _typeMap[DafnyTokenKinds.TypeIdentifier] = typeService.GetClassificationType("Dafny user type"); + _typeMap[DafnyTokenKinds.VariableIdentifierDefinition] = typeService.GetClassificationType("Dafny identifier"); } public event EventHandler TagsChanged; @@ -82,16 +82,16 @@ namespace DafnyLanguage /// Defines an editor format for user-defined type. /// [Export(typeof(EditorFormatDefinition))] - [ClassificationType(ClassificationTypeNames = "Dafny user type")] - [Name("Dafny user type")] + [ClassificationType(ClassificationTypeNames = "Dafny identifier")] + [Name("Dafny identifier")] [UserVisible(true)] //set the priority to be after the default classifiers [Order(Before = Priority.Default)] internal sealed class DafnyTypeFormat : ClassificationFormatDefinition { public DafnyTypeFormat() { - this.DisplayName = "Dafny user type"; //human readable version of the name - this.ForegroundColor = Colors.Coral; + this.DisplayName = "Dafny identifier"; //human readable version of the name + this.ForegroundColor = Colors.CornflowerBlue; } } @@ -101,7 +101,7 @@ namespace DafnyLanguage /// Defines the "ordinary" classification type. /// [Export(typeof(ClassificationTypeDefinition))] - [Name("Dafny user type")] + [Name("Dafny identifier")] internal static ClassificationTypeDefinition UserType = null; } } diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj index cfa7a070..66370dec 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj +++ b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj @@ -128,6 +128,8 @@ + + diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/HoverText.cs b/Util/VS2010/DafnyExtension/DafnyExtension/HoverText.cs new file mode 100644 index 00000000..de0721ec --- /dev/null +++ b/Util/VS2010/DafnyExtension/DafnyExtension/HoverText.cs @@ -0,0 +1,134 @@ +using System; +using System.Collections.Generic; +using System.Linq; +using System.Text; +using System.Windows.Input; +using Microsoft.VisualStudio.Language.Intellisense; +using System.Collections.ObjectModel; +using Microsoft.VisualStudio.Text; +using Microsoft.VisualStudio.Text.Editor; +using Microsoft.VisualStudio.Text.Tagging; +using System.ComponentModel.Composition; +using Microsoft.VisualStudio.Utilities; +using System.Diagnostics.Contracts; + + +namespace DafnyLanguage +{ + [Export(typeof(IQuickInfoSourceProvider))] + [ContentType("dafny")] + [Name("Dafny QuickInfo")] + class OokQuickInfoSourceProvider : IQuickInfoSourceProvider + { + [Import] + IBufferTagAggregatorFactoryService aggService = null; + + public IQuickInfoSource TryCreateQuickInfoSource(ITextBuffer textBuffer) { + return new OokQuickInfoSource(textBuffer, aggService.CreateTagAggregator(textBuffer)); + } + } + + class OokQuickInfoSource : IQuickInfoSource + { + private ITagAggregator _aggregator; + private ITextBuffer _buffer; + private bool _disposed = false; + + + public OokQuickInfoSource(ITextBuffer buffer, ITagAggregator aggregator) { + _aggregator = aggregator; + _buffer = buffer; + } + + public void AugmentQuickInfoSession(IQuickInfoSession session, IList quickInfoContent, out ITrackingSpan applicableToSpan) { + applicableToSpan = null; + + if (_disposed) + throw new ObjectDisposedException("TestQuickInfoSource"); + + var triggerPoint = (SnapshotPoint)session.GetTriggerPoint(_buffer.CurrentSnapshot); + + if (triggerPoint == null) + return; + + foreach (IMappingTagSpan curTag in _aggregator.GetTags(new SnapshotSpan(triggerPoint, triggerPoint))) { + var s = curTag.Tag.HoverText; + if (s != null) { + var tagSpan = curTag.Span.GetSpans(_buffer).First(); + applicableToSpan = _buffer.CurrentSnapshot.CreateTrackingSpan(tagSpan, SpanTrackingMode.EdgeExclusive); + quickInfoContent.Add(s); + } + } + } + + public void Dispose() { + _disposed = true; + } + } + // --------------------------------- QuickInfo controller ------------------------------------------ + + [Export(typeof(IIntellisenseControllerProvider))] + [Name("Dafny QuickInfo controller")] + [ContentType("dafny")] + class DafnyQuickInfoControllerProvider : IIntellisenseControllerProvider + { + [Import] + internal IQuickInfoBroker QuickInfoBroker { get; set; } + + public IIntellisenseController TryCreateIntellisenseController(ITextView textView, IList subjectBuffers) { + return new DafnyQuickInfoController(textView, subjectBuffers, this); + } + } + + class DafnyQuickInfoController : IIntellisenseController + { + private ITextView _textView; + private IList _subjectBuffers; + private DafnyQuickInfoControllerProvider _componentContext; + + private IQuickInfoSession _session; + + internal DafnyQuickInfoController(ITextView textView, IList subjectBuffers, DafnyQuickInfoControllerProvider componentContext) { + _textView = textView; + _subjectBuffers = subjectBuffers; + _componentContext = componentContext; + + _textView.MouseHover += this.OnTextViewMouseHover; + } + + public void ConnectSubjectBuffer(ITextBuffer subjectBuffer) { + } + + public void DisconnectSubjectBuffer(ITextBuffer subjectBuffer) { + } + + public void Detach(ITextView textView) { + if (_textView == textView) { + _textView.MouseHover -= OnTextViewMouseHover; + _textView = null; + } + } + + void OnTextViewMouseHover(object sender, MouseHoverEventArgs e) { + SnapshotPoint? point = GetMousePosition(new SnapshotPoint(_textView.TextSnapshot, e.Position)); + + if (point != null) { + ITrackingPoint triggerPoint = point.Value.Snapshot.CreateTrackingPoint(point.Value.Position, PointTrackingMode.Positive); + + // Find the broker for this buffer + if (!_componentContext.QuickInfoBroker.IsQuickInfoActive(_textView)) { + _session = _componentContext.QuickInfoBroker.CreateQuickInfoSession(_textView, triggerPoint, true); + _session.Start(); + } + } + } + + SnapshotPoint? GetMousePosition(SnapshotPoint topPosition) { + return _textView.BufferGraph.MapDownToFirstMatch( + topPosition, + PointTrackingMode.Positive, + snapshot => _subjectBuffers.Contains(snapshot.TextBuffer), + PositionAffinity.Predecessor); + } + } +} 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 CreateTagger(ITextBuffer buffer) where T : ITag { + ITagAggregator tagAggregator = AggregatorFactory.CreateTagAggregator(buffer); + // create a single tagger for each buffer. + Func> sc = delegate() { return new IdentifierTagger(buffer, tagAggregator) as ITagger; }; + return buffer.Properties.GetOrCreateSingletonProperty>(sc); + } + } + + /// + /// Translate DafnyResolverTag's into IOutliningRegionTag's + /// + internal sealed class IdentifierTagger : ITagger + { + 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 _regions = new List(); // the regions generated from _program + ITagAggregator _aggregator; + + internal IdentifierTagger(ITextBuffer buffer, ITagAggregator tagAggregator) { + _buffer = buffer; + _snapshot = _buffer.CurrentSnapshot; + _aggregator = tagAggregator; + _aggregator.TagsChanged += new EventHandler(_aggregator_TagsChanged); + } + + /// + /// 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; + // (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( + 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 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 newRegions = new List(); + + 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 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 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; + } + } + } + +} diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs index 10bb36e1..2017cfaa 100644 --- a/Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs +++ b/Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs @@ -186,7 +186,6 @@ namespace DafnyLanguage _errorProvider.Tasks.Clear(); foreach (var err in AllErrors()) { ErrorTask task = new ErrorTask() { - // CanDelete = true, Category = TaskCategory.BuildCompile, ErrorCategory = CategoryConversion(err.Category), Text = err.Message, -- cgit v1.2.3