diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-10-04 13:32:50 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-10-04 13:32:50 -0700 |
| commit | 8911e5c95d4715c2e2626aef67f19793d6f43201 (patch) | |
| tree | d703bfd931802e780430e32f1339cf77adc342a4 /Source/DafnyExtension | |
| parent | 1c375d1889e628fcd2a1a0fc041673a5f4230d84 (diff) | |
Put all sources under \Source directory
Diffstat (limited to 'Source/DafnyExtension')
| -rw-r--r-- | Source/DafnyExtension/BraceMatching.cs | 253 | ||||
| -rw-r--r-- | Source/DafnyExtension/BufferIdleEventUtil.cs | 155 | ||||
| -rw-r--r-- | Source/DafnyExtension/ClassificationTagger.cs | 107 | ||||
| -rw-r--r-- | Source/DafnyExtension/ContentType.cs | 18 | ||||
| -rw-r--r-- | Source/DafnyExtension/DafnyDriver.cs | 419 | ||||
| -rw-r--r-- | Source/DafnyExtension/DafnyExtension.csproj | 191 | ||||
| -rw-r--r-- | Source/DafnyExtension/ErrorTagger.cs | 85 | ||||
| -rw-r--r-- | Source/DafnyExtension/HoverText.cs | 126 | ||||
| -rw-r--r-- | Source/DafnyExtension/IdentifierTagger.cs | 344 | ||||
| -rw-r--r-- | Source/DafnyExtension/OutliningTagger.cs | 185 | ||||
| -rw-r--r-- | Source/DafnyExtension/ProgressMargin.cs | 260 | ||||
| -rw-r--r-- | Source/DafnyExtension/Properties/AssemblyInfo.cs | 33 | ||||
| -rw-r--r-- | Source/DafnyExtension/ResolverTagger.cs | 321 | ||||
| -rw-r--r-- | Source/DafnyExtension/TokenTagger.cs | 342 | ||||
| -rw-r--r-- | Source/DafnyExtension/WordHighlighter.cs | 211 | ||||
| -rw-r--r-- | Source/DafnyExtension/source.extension.vsixmanifest | 25 |
16 files changed, 3075 insertions, 0 deletions
diff --git a/Source/DafnyExtension/BraceMatching.cs b/Source/DafnyExtension/BraceMatching.cs new file mode 100644 index 00000000..44b1affe --- /dev/null +++ b/Source/DafnyExtension/BraceMatching.cs @@ -0,0 +1,253 @@ +using System;
+using System.Linq;
+using System.Collections.Generic;
+using System.ComponentModel.Composition;
+using Microsoft.VisualStudio.Text;
+using Microsoft.VisualStudio.Text.Editor;
+using Microsoft.VisualStudio.Text.Tagging;
+using Microsoft.VisualStudio.Utilities;
+
+namespace DafnyLanguage
+{
+ [Export(typeof(IViewTaggerProvider))]
+ [ContentType("dafny")]
+ [TagType(typeof(TextMarkerTag))]
+ internal class BraceMatchingTaggerProvider : IViewTaggerProvider
+ {
+ [Import]
+ internal IBufferTagAggregatorFactoryService AggregatorFactory = null;
+
+ public ITagger<T> CreateTagger<T>(ITextView textView, ITextBuffer buffer) where T : ITag {
+ if (textView == null)
+ return null;
+
+ //provide highlighting only on the top-level buffer
+ if (textView.TextBuffer != buffer)
+ return null;
+
+ ITagAggregator<DafnyTokenTag> tagAggregator = AggregatorFactory.CreateTagAggregator<DafnyTokenTag>(buffer);
+ return new BraceMatchingTagger(textView, buffer, tagAggregator) as ITagger<T>;
+ }
+ }
+
+ internal abstract class TokenBasedTagger
+ {
+ ITagAggregator<DafnyTokenTag> _aggregator;
+
+ internal TokenBasedTagger(ITagAggregator<DafnyTokenTag> tagAggregator) {
+ _aggregator = tagAggregator;
+ }
+
+ public bool InsideComment(SnapshotPoint pt) {
+ SnapshotSpan span = new SnapshotSpan(pt, 1);
+ foreach (var tagSpan in this._aggregator.GetTags(span)) {
+ switch (tagSpan.Tag.Kind) {
+ case DafnyTokenKinds.Comment:
+ case DafnyTokenKinds.String:
+ foreach (var s in tagSpan.Span.GetSpans(pt.Snapshot)) {
+ if (s.Contains(span))
+ return true;
+ }
+ break;
+ default:
+ break;
+ }
+ }
+ return false;
+ }
+ }
+
+ internal class BraceMatchingTagger : TokenBasedTagger, ITagger<TextMarkerTag>
+ {
+ ITextView View { get; set; }
+ ITextBuffer SourceBuffer { get; set; }
+ SnapshotPoint? CurrentChar { get; set; }
+ private char[] openBraces;
+ private char[] closeBraces;
+
+ static TextMarkerTag Blue = new TextMarkerTag("blue");
+
+ internal BraceMatchingTagger(ITextView view, ITextBuffer sourceBuffer, ITagAggregator<DafnyTokenTag> tagAggregator)
+ : base(tagAggregator)
+ {
+ //here the keys are the open braces, and the values are the close braces
+ openBraces = new char[] { '(', '{', '[' };
+ closeBraces = new char[] { ')', '}', ']' };
+ this.View = view;
+ this.SourceBuffer = sourceBuffer;
+ this.CurrentChar = null;
+
+ this.View.Caret.PositionChanged += CaretPositionChanged;
+ this.View.LayoutChanged += ViewLayoutChanged;
+ }
+
+ public event EventHandler<SnapshotSpanEventArgs> TagsChanged;
+
+ void ViewLayoutChanged(object sender, TextViewLayoutChangedEventArgs e) {
+ if (e.NewSnapshot != e.OldSnapshot) //make sure that there has really been a change
+ {
+ UpdateAtCaretPosition(View.Caret.Position);
+ }
+ }
+
+ void CaretPositionChanged(object sender, CaretPositionChangedEventArgs e) {
+ UpdateAtCaretPosition(e.NewPosition);
+ }
+
+ void UpdateAtCaretPosition(CaretPosition caretPosition) {
+ CurrentChar = caretPosition.Point.GetPoint(SourceBuffer, caretPosition.Affinity);
+
+ if (!CurrentChar.HasValue)
+ return;
+
+ var chngd = TagsChanged;
+ if (chngd != null)
+ chngd(this, new SnapshotSpanEventArgs(new SnapshotSpan(SourceBuffer.CurrentSnapshot, 0, SourceBuffer.CurrentSnapshot.Length)));
+ }
+
+ public IEnumerable<ITagSpan<TextMarkerTag>> GetTags(NormalizedSnapshotSpanCollection spans) {
+ if (spans.Count == 0) //there is no content in the buffer
+ yield break;
+
+ //don't do anything if the current SnapshotPoint is not initialized
+ if (!CurrentChar.HasValue)
+ yield break;
+
+ //hold on to a snapshot of the current character
+ SnapshotPoint currentChar = CurrentChar.Value;
+
+ //if the requested snapshot isn't the same as the one the brace is on, translate our spans to the expected snapshot
+ if (spans[0].Snapshot != currentChar.Snapshot) {
+ currentChar = currentChar.TranslateTo(spans[0].Snapshot, PointTrackingMode.Positive);
+ }
+
+ if (currentChar.Position < spans[0].Snapshot.Length) {
+ // Check if the current character is an open brace
+ char ch = currentChar.GetChar();
+ char closeCh;
+ if (MatchBrace(currentChar, ch, true, out closeCh)) {
+ SnapshotSpan pairSpan;
+ if (FindMatchingCloseChar(currentChar, ch, closeCh, View.TextViewLines.Count, out pairSpan)) {
+ yield return new TagSpan<TextMarkerTag>(new SnapshotSpan(currentChar, 1), Blue);
+ yield return new TagSpan<TextMarkerTag>(pairSpan, Blue);
+ }
+ }
+ }
+
+ if (0 < currentChar.Position) {
+ // Check if the previous character is a close brace (note, caret may be between a close brace and an open brace, in which case we'll tag two pairs)
+ SnapshotPoint prevChar = currentChar - 1;
+ char ch = prevChar.GetChar();
+ char openCh;
+ if (MatchBrace(prevChar, ch, false, out openCh)) {
+ SnapshotSpan pairSpan;
+ if (FindMatchingOpenChar(prevChar, openCh, ch, View.TextViewLines.Count, out pairSpan)) {
+ yield return new TagSpan<TextMarkerTag>(new SnapshotSpan(prevChar, 1), Blue);
+ yield return new TagSpan<TextMarkerTag>(pairSpan, Blue);
+ }
+ }
+ }
+ }
+
+ private bool MatchBrace(SnapshotPoint pt, char query, bool sourceIsOpen, out char match) {
+ if (!InsideComment(pt)) {
+ char[] source = sourceIsOpen ? openBraces : closeBraces;
+ int i = 0;
+ foreach (char ch in source) {
+ if (ch == query) {
+ char[] dest = sourceIsOpen ? closeBraces : openBraces;
+ match = dest[i];
+ return true;
+ }
+ i++;
+ }
+ }
+ match = query; // satisfy compiler
+ return false;
+ }
+
+ private bool FindMatchingCloseChar(SnapshotPoint startPoint, char open, char close, int linesViewed, out SnapshotSpan pairSpan) {
+ ITextSnapshotLine line = startPoint.GetContainingLine();
+ int lineNumber = line.LineNumber;
+ int offset = startPoint.Position - line.Start.Position + 1;
+
+ int lineNumberLimit = Math.Min(startPoint.Snapshot.LineCount, lineNumber + linesViewed);
+
+ int openCount = 0;
+ while (true) {
+ string lineText = line.GetText();
+
+ //walk the entire line
+ for (; offset < line.Length; offset++) {
+ char currentChar = lineText[offset];
+ if (currentChar == open || currentChar == close) {
+ if (!InsideComment(new SnapshotPoint(line.Snapshot, line.Start.Position + offset))) {
+ if (currentChar == open) {
+ openCount++;
+ } else if (0 < openCount) {
+ openCount--;
+ } else {
+ //found the matching close
+ pairSpan = new SnapshotSpan(startPoint.Snapshot, line.Start + offset, 1);
+ return true;
+ }
+ }
+ }
+ }
+
+ //move on to the next line
+ lineNumber++;
+ if (lineNumberLimit <= lineNumber)
+ break;
+
+ line = line.Snapshot.GetLineFromLineNumber(lineNumber);
+ offset = 0;
+ }
+
+ pairSpan = new SnapshotSpan(startPoint, startPoint); // satisfy the compiler
+ return false;
+ }
+
+ private bool FindMatchingOpenChar(SnapshotPoint startPoint, char open, char close, int linesViewed, out SnapshotSpan pairSpan) {
+ ITextSnapshotLine line = startPoint.GetContainingLine();
+ int lineNumber = line.LineNumber;
+ int offset = startPoint.Position - line.Start.Position - 1; //move the offset to the character before this one
+
+ int lineNumberLimit = Math.Max(0, lineNumber - linesViewed);
+
+ int closeCount = 0;
+ while (true) {
+ string lineText = line.GetText();
+
+ //walk the entire line
+ for (; 0 <= offset; offset--) {
+ char currentChar = lineText[offset];
+ if (currentChar == open || currentChar == close) {
+ if (!InsideComment(new SnapshotPoint(line.Snapshot, line.Start.Position + offset))) {
+ if (currentChar == close) {
+ closeCount++;
+ } else if (0 < closeCount) {
+ closeCount--;
+ } else {
+ // We've found the open character
+ pairSpan = new SnapshotSpan(line.Start + offset, 1); //we just want the character itself
+ return true;
+ }
+ }
+ }
+ }
+
+ // Move to the previous line
+ lineNumber--;
+ if (lineNumber < lineNumberLimit)
+ break;
+
+ line = line.Snapshot.GetLineFromLineNumber(lineNumber);
+ offset = line.Length - 1;
+ }
+
+ pairSpan = new SnapshotSpan(startPoint, startPoint); // satisfy the compiler
+ return false;
+ }
+ }
+}
diff --git a/Source/DafnyExtension/BufferIdleEventUtil.cs b/Source/DafnyExtension/BufferIdleEventUtil.cs new file mode 100644 index 00000000..1aea1385 --- /dev/null +++ b/Source/DafnyExtension/BufferIdleEventUtil.cs @@ -0,0 +1,155 @@ +//***************************************************************************
+// 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 System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.VisualStudio.Text;
+using System.Windows.Threading;
+
+namespace DafnyLanguage
+{
+ /// <summary>
+ /// Handy reusable utility to listen for change events on the associated buffer, but
+ /// only pass these along to a set of listeners when the user stops typing for a half second
+ /// </summary>
+ static class BufferIdleEventUtil
+ {
+ static object bufferListenersKey = new object();
+ static object bufferTimerKey = new object();
+
+ #region Public interface
+
+ public static bool AddBufferIdleEventListener(ITextBuffer buffer, EventHandler handler)
+ {
+ HashSet<EventHandler> listenersForBuffer;
+ if (!TryGetBufferListeners(buffer, out listenersForBuffer))
+ listenersForBuffer = ConnectToBuffer(buffer);
+
+ if (listenersForBuffer.Contains(handler))
+ return false;
+
+ listenersForBuffer.Add(handler);
+
+ return true;
+ }
+
+ public static bool RemoveBufferIdleEventListener(ITextBuffer buffer, EventHandler handler)
+ {
+ HashSet<EventHandler> listenersForBuffer;
+ if (!TryGetBufferListeners(buffer, out listenersForBuffer))
+ return false;
+
+ if (!listenersForBuffer.Contains(handler))
+ return false;
+
+ listenersForBuffer.Remove(handler);
+
+ if (listenersForBuffer.Count == 0)
+ DisconnectFromBuffer(buffer);
+
+ return true;
+ }
+
+ #endregion
+
+ #region Helpers
+
+ static bool TryGetBufferListeners(ITextBuffer buffer, out HashSet<EventHandler> listeners)
+ {
+ return buffer.Properties.TryGetProperty(bufferListenersKey, out listeners);
+ }
+
+ static void ClearBufferListeners(ITextBuffer buffer)
+ {
+ buffer.Properties.RemoveProperty(bufferListenersKey);
+ }
+
+ static bool TryGetBufferTimer(ITextBuffer buffer, out DispatcherTimer timer)
+ {
+ return buffer.Properties.TryGetProperty(bufferTimerKey, out timer);
+ }
+
+ static void ClearBufferTimer(ITextBuffer buffer)
+ {
+ DispatcherTimer timer;
+ if (TryGetBufferTimer(buffer, out timer))
+ {
+ if (timer != null)
+ timer.Stop();
+ buffer.Properties.RemoveProperty(bufferTimerKey);
+ }
+ }
+
+ static void DisconnectFromBuffer(ITextBuffer buffer)
+ {
+ buffer.Changed -= BufferChanged;
+
+ ClearBufferListeners(buffer);
+ ClearBufferTimer(buffer);
+
+ buffer.Properties.RemoveProperty(bufferListenersKey);
+ }
+
+ static HashSet<EventHandler> ConnectToBuffer(ITextBuffer buffer)
+ {
+ buffer.Changed += BufferChanged;
+
+ RestartTimerForBuffer(buffer);
+
+ HashSet<EventHandler> listenersForBuffer = new HashSet<EventHandler>();
+ buffer.Properties[bufferListenersKey] = listenersForBuffer;
+
+ return listenersForBuffer;
+ }
+
+ static void RestartTimerForBuffer(ITextBuffer buffer)
+ {
+ DispatcherTimer timer;
+
+ if (TryGetBufferTimer(buffer, out timer))
+ {
+ timer.Stop();
+ }
+ else
+ {
+ timer = new DispatcherTimer(DispatcherPriority.ApplicationIdle)
+ {
+ Interval = TimeSpan.FromMilliseconds(500)
+ };
+
+ timer.Tick += (s, e) =>
+ {
+ ClearBufferTimer(buffer);
+
+ HashSet<EventHandler> handlers;
+ if (TryGetBufferListeners(buffer, out handlers))
+ {
+ foreach (var handler in handlers)
+ {
+ handler(buffer, new EventArgs());
+ }
+ }
+ };
+
+ buffer.Properties[bufferTimerKey] = timer;
+ }
+
+ timer.Start();
+ }
+
+ static void BufferChanged(object sender, TextContentChangedEventArgs e)
+ {
+ ITextBuffer buffer = sender as ITextBuffer;
+ if (buffer == null)
+ return;
+
+ RestartTimerForBuffer(buffer);
+ }
+
+ #endregion
+ }
+}
diff --git a/Source/DafnyExtension/ClassificationTagger.cs b/Source/DafnyExtension/ClassificationTagger.cs new file mode 100644 index 00000000..09835ac9 --- /dev/null +++ b/Source/DafnyExtension/ClassificationTagger.cs @@ -0,0 +1,107 @@ +using System;
+using System.Collections.Generic;
+using System.ComponentModel.Composition;
+using System.Windows.Media;
+using Microsoft.VisualStudio.Text;
+using Microsoft.VisualStudio.Text.Classification;
+using Microsoft.VisualStudio.Text.Editor;
+using Microsoft.VisualStudio.Text.Tagging;
+using Microsoft.VisualStudio.Utilities;
+
+
+namespace DafnyLanguage
+{
+ [Export(typeof(ITaggerProvider))]
+ [ContentType("dafny")]
+ [TagType(typeof(ClassificationTag))]
+ internal sealed class DafnyClassifierProvider : ITaggerProvider
+ {
+ [Import]
+ internal IBufferTagAggregatorFactoryService AggregatorFactory = null;
+
+ [Import]
+ internal IClassificationTypeRegistryService ClassificationTypeRegistry = null;
+
+ [Import]
+ internal Microsoft.VisualStudio.Language.StandardClassification.IStandardClassificationService Standards = null;
+
+ public ITagger<T> CreateTagger<T>(ITextBuffer buffer) where T : ITag {
+ ITagAggregator<DafnyTokenTag> tagAggregator = AggregatorFactory.CreateTagAggregator<DafnyTokenTag>(buffer);
+ return new DafnyClassifier(buffer, tagAggregator, ClassificationTypeRegistry, Standards) as ITagger<T>;
+ }
+ }
+
+ internal sealed class DafnyClassifier : ITagger<ClassificationTag>
+ {
+ ITextBuffer _buffer;
+ ITagAggregator<DafnyTokenTag> _aggregator;
+ IDictionary<DafnyTokenKinds, IClassificationType> _typeMap;
+
+ internal DafnyClassifier(ITextBuffer buffer,
+ ITagAggregator<DafnyTokenTag> tagAggregator,
+ IClassificationTypeRegistryService typeService, Microsoft.VisualStudio.Language.StandardClassification.IStandardClassificationService standards) {
+ _buffer = buffer;
+ _aggregator = tagAggregator;
+ _aggregator.TagsChanged += new EventHandler<TagsChangedEventArgs>(_aggregator_TagsChanged);
+ // use built-in classification types:
+ _typeMap = new Dictionary<DafnyTokenKinds, IClassificationType>();
+ _typeMap[DafnyTokenKinds.Keyword] = standards.Keyword;
+ _typeMap[DafnyTokenKinds.Number] = standards.NumberLiteral;
+ _typeMap[DafnyTokenKinds.String] = standards.StringLiteral;
+ _typeMap[DafnyTokenKinds.Comment] = standards.Comment;
+ _typeMap[DafnyTokenKinds.VariableIdentifier] = standards.Identifier;
+ _typeMap[DafnyTokenKinds.VariableIdentifierDefinition] = typeService.GetClassificationType("Dafny identifier");
+ }
+
+ public event EventHandler<SnapshotSpanEventArgs> TagsChanged;
+
+ public IEnumerable<ITagSpan<ClassificationTag>> GetTags(NormalizedSnapshotSpanCollection spans) {
+ if (spans.Count == 0) yield break;
+ var snapshot = spans[0].Snapshot;
+ foreach (var tagSpan in this._aggregator.GetTags(spans)) {
+ IClassificationType t = _typeMap[tagSpan.Tag.Kind];
+ foreach (SnapshotSpan s in tagSpan.Span.GetSpans(snapshot)) {
+ yield return new TagSpan<ClassificationTag>(s, new ClassificationTag(t));
+ }
+ }
+ }
+
+ void _aggregator_TagsChanged(object sender, TagsChangedEventArgs e) {
+ 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));
+ }
+ }
+ }
+ }
+
+ /// <summary>
+ /// Defines an editor format for user-defined type.
+ /// </summary>
+ [Export(typeof(EditorFormatDefinition))]
+ [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 identifier"; //human readable version of the name
+ this.ForegroundColor = Colors.CornflowerBlue;
+ }
+ }
+
+ internal static class ClassificationDefinition
+ {
+ /// <summary>
+ /// Defines the "ordinary" classification type.
+ /// </summary>
+ [Export(typeof(ClassificationTypeDefinition))]
+ [Name("Dafny identifier")]
+ internal static ClassificationTypeDefinition UserType = null;
+ }
+}
diff --git a/Source/DafnyExtension/ContentType.cs b/Source/DafnyExtension/ContentType.cs new file mode 100644 index 00000000..d8487f74 --- /dev/null +++ b/Source/DafnyExtension/ContentType.cs @@ -0,0 +1,18 @@ +using System.ComponentModel.Composition;
+using Microsoft.VisualStudio.Utilities;
+
+namespace DafnyLanguage
+{
+ class DafnyContentType
+ {
+ [Export]
+ [Name("dafny")]
+ [BaseDefinition("code")]
+ internal static ContentTypeDefinition ContentType = null;
+
+ [Export]
+ [FileExtension(".dfy")]
+ [ContentType("dafny")]
+ internal static FileExtensionToContentTypeDefinition FileType = null;
+ }
+}
diff --git a/Source/DafnyExtension/DafnyDriver.cs b/Source/DafnyExtension/DafnyDriver.cs new file mode 100644 index 00000000..39829bb0 --- /dev/null +++ b/Source/DafnyExtension/DafnyDriver.cs @@ -0,0 +1,419 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.IO;
+using System.Diagnostics;
+using System.Diagnostics.Contracts;
+// Here come the Dafny/Boogie specific imports
+//using PureCollections;
+using Bpl = Microsoft.Boogie;
+using Dafny = Microsoft.Dafny;
+using Microsoft.Boogie.AbstractInterpretation;
+using VC;
+// using AI = Microsoft.AbstractInterpretationFramework;
+
+
+namespace DafnyLanguage
+{
+ class DafnyDriver
+ {
+ readonly string _programText;
+ readonly string _filename;
+ Dafny.Program _program;
+ List<DafnyError> _errors = new List<DafnyError>();
+ public List<DafnyError> Errors { get { return _errors; } }
+
+ public DafnyDriver(string programText, string filename) {
+ _programText = programText;
+ _filename = filename;
+ }
+
+ void RecordError(int line, int col, ErrorCategory cat, string msg) {
+ _errors.Add(new DafnyError(line, col, cat, msg));
+ }
+
+ static DafnyDriver() {
+ Initialize();
+ }
+
+ static void Initialize() {
+ if (Dafny.DafnyOptions.O == null) {
+ var options = new Dafny.DafnyOptions();
+ options.ProverKillTime = 10;
+ options.ErrorTrace = 0;
+ Dafny.DafnyOptions.Install(options);
+ options.ApplyDefaultOptions();
+ }
+ }
+
+ public Dafny.Program ProcessResolution() {
+ if (!ParseAndTypeCheck()) {
+ return null;
+ }
+ return _program;
+ }
+
+ bool ParseAndTypeCheck() {
+ Dafny.ModuleDecl module = new Dafny.LiteralModuleDecl(new Dafny.DefaultModuleDecl(), null);
+ Dafny.BuiltIns builtIns = new Dafny.BuiltIns();
+ int errorCount = Dafny.Parser.Parse(_programText, _filename, module, builtIns, new VSErrors(this));
+ if (errorCount != 0)
+ return false;
+ Dafny.Program program = new Dafny.Program(_filename, module, builtIns);
+
+ Dafny.Resolver r = new VSResolver(program, this);
+ r.ResolveProgram(program);
+ if (r.ErrorCount != 0)
+ return false;
+
+ _program = program;
+ return true; // success
+ }
+
+ class VSErrors : Dafny.Errors
+ {
+ DafnyDriver dd;
+ public VSErrors(DafnyDriver dd) {
+ this.dd = dd;
+ }
+ public override void SynErr(string filename, int line, int col, string msg) {
+ dd.RecordError(line - 1, col - 1, ErrorCategory.ParseError, msg);
+ count++;
+ }
+ public override void SemErr(string filename, int line, int col, string msg) {
+ dd.RecordError(line - 1, col - 1, ErrorCategory.ResolveError, msg);
+ count++;
+ }
+ public override void Warning(string filename, int line, int col, string msg) {
+ dd.RecordError(line - 1, col - 1, ErrorCategory.ParseWarning, msg);
+ }
+ }
+
+ class VSResolver : Dafny.Resolver
+ {
+ DafnyDriver dd;
+ public VSResolver(Dafny.Program program, DafnyDriver dd)
+ : base(program) {
+ this.dd = dd;
+ }
+ public override void Error(Bpl.IToken tok, string msg, params object[] args) {
+ string s = string.Format(msg, args);
+ dd.RecordError(tok.line - 1, tok.col - 1, ErrorCategory.ResolveError, s);
+ ErrorCount++;
+ }
+ }
+
+ public static bool Verify(Dafny.Program dafnyProgram, ErrorReporterDelegate er) {
+ Dafny.Translator translator = new Dafny.Translator();
+ Bpl.Program boogieProgram = translator.Translate(dafnyProgram);
+
+ PipelineOutcome oc = BoogiePipeline(boogieProgram, er);
+ switch (oc) {
+ case PipelineOutcome.Done:
+ case PipelineOutcome.VerificationCompleted:
+ // TODO: This would be the place to proceed to compile the program, if desired
+ return true;
+ case PipelineOutcome.FatalError:
+ default:
+ return false;
+ }
+ }
+
+ enum PipelineOutcome { Done, ResolutionError, TypeCheckingError, ResolvedAndTypeChecked, FatalError, VerificationCompleted }
+
+ /// <summary>
+ /// Resolve, type check, infer invariants for, and verify the given Boogie program.
+ /// The intention is that this Boogie program has been produced by translation from something
+ /// else. Hence, any resolution errors and type checking errors are due to errors in
+ /// the translation.
+ /// </summary>
+ static PipelineOutcome BoogiePipeline(Bpl.Program/*!*/ program, ErrorReporterDelegate er) {
+ Contract.Requires(program != null);
+
+ PipelineOutcome oc = BoogieResolveAndTypecheck(program);
+ if (oc == PipelineOutcome.ResolvedAndTypeChecked) {
+ EliminateDeadVariablesAndInline(program);
+ return BoogieInferAndVerify(program, er);
+ }
+ return oc;
+ }
+
+ static void EliminateDeadVariablesAndInline(Bpl.Program program) {
+ Contract.Requires(program != null);
+ // Eliminate dead variables
+ Microsoft.Boogie.UnusedVarEliminator.Eliminate(program);
+
+ // Collect mod sets
+ if (Bpl.CommandLineOptions.Clo.DoModSetAnalysis) {
+ Microsoft.Boogie.ModSetCollector.DoModSetAnalysis(program);
+ }
+
+ // Coalesce blocks
+ if (Bpl.CommandLineOptions.Clo.CoalesceBlocks) {
+ Microsoft.Boogie.BlockCoalescer.CoalesceBlocks(program);
+ }
+
+ // Inline
+ var TopLevelDeclarations = program.TopLevelDeclarations;
+
+ if (Bpl.CommandLineOptions.Clo.ProcedureInlining != Bpl.CommandLineOptions.Inlining.None) {
+ bool inline = false;
+ foreach (var d in TopLevelDeclarations) {
+ if (d.FindExprAttribute("inline") != null) {
+ inline = true;
+ }
+ }
+ if (inline && Bpl.CommandLineOptions.Clo.StratifiedInlining == 0) {
+ foreach (var d in TopLevelDeclarations) {
+ var impl = d as Bpl.Implementation;
+ if (impl != null) {
+ impl.OriginalBlocks = impl.Blocks;
+ impl.OriginalLocVars = impl.LocVars;
+ }
+ }
+ foreach (var d in TopLevelDeclarations) {
+ var impl = d as Bpl.Implementation;
+ if (impl != null && !impl.SkipVerification) {
+ Bpl.Inliner.ProcessImplementation(program, impl);
+ }
+ }
+ foreach (var d in TopLevelDeclarations) {
+ var impl = d as Bpl.Implementation;
+ if (impl != null) {
+ impl.OriginalBlocks = null;
+ impl.OriginalLocVars = null;
+ }
+ }
+ }
+ }
+ }
+
+ /// <summary>
+ /// Resolves and type checks the given Boogie program.
+ /// Returns:
+ /// - Done if no errors occurred, and command line specified no resolution or no type checking.
+ /// - ResolutionError if a resolution error occurred
+ /// - TypeCheckingError if a type checking error occurred
+ /// - ResolvedAndTypeChecked if both resolution and type checking succeeded
+ /// </summary>
+ static PipelineOutcome BoogieResolveAndTypecheck(Bpl.Program program) {
+ Contract.Requires(program != null);
+ // ---------- Resolve ------------------------------------------------------------
+ int errorCount = program.Resolve();
+ if (errorCount != 0) {
+ return PipelineOutcome.ResolutionError;
+ }
+
+ // ---------- Type check ------------------------------------------------------------
+ errorCount = program.Typecheck();
+ if (errorCount != 0) {
+ return PipelineOutcome.TypeCheckingError;
+ }
+
+ return PipelineOutcome.ResolvedAndTypeChecked;
+ }
+
+ /// <summary>
+ /// Given a resolved and type checked Boogie program, infers invariants for the program
+ /// and then attempts to verify it. Returns:
+ /// - Done if command line specified no verification
+ /// - FatalError if a fatal error occurred
+ /// - VerificationCompleted if inference and verification completed, in which the out
+ /// parameters contain meaningful values
+ /// </summary>
+ static PipelineOutcome BoogieInferAndVerify(Bpl.Program program, ErrorReporterDelegate er) {
+ Contract.Requires(program != null);
+
+ // ---------- Infer invariants --------------------------------------------------------
+
+ // Abstract interpretation -> Always use (at least) intervals, if not specified otherwise (e.g. with the "/noinfer" switch)
+ if (Bpl.CommandLineOptions.Clo.UseAbstractInterpretation) {
+ if (Bpl.CommandLineOptions.Clo.Ai.J_Intervals || Bpl.CommandLineOptions.Clo.Ai.J_Trivial) {
+ Microsoft.Boogie.AbstractInterpretation.NativeAbstractInterpretation.RunAbstractInterpretation(program);
+ } else {
+ // use /infer:j as the default
+ Bpl.CommandLineOptions.Clo.Ai.J_Intervals = true;
+ Microsoft.Boogie.AbstractInterpretation.NativeAbstractInterpretation.RunAbstractInterpretation(program);
+ }
+ }
+
+ if (Bpl.CommandLineOptions.Clo.LoopUnrollCount != -1) {
+ program.UnrollLoops(Bpl.CommandLineOptions.Clo.LoopUnrollCount);
+ }
+
+ if (Bpl.CommandLineOptions.Clo.ExpandLambdas) {
+ Bpl.LambdaHelper.ExpandLambdas(program);
+ //PrintBplFile ("-", program, true);
+ }
+
+ // ---------- Verify ------------------------------------------------------------
+
+ if (!Bpl.CommandLineOptions.Clo.Verify) { return PipelineOutcome.Done; }
+
+ #region Verify each implementation
+
+ ConditionGeneration vcgen = null;
+ try {
+ vcgen = new VCGen(program, Bpl.CommandLineOptions.Clo.SimplifyLogFilePath, Bpl.CommandLineOptions.Clo.SimplifyLogFileAppend);
+ } catch (Bpl.ProverException) {
+ return PipelineOutcome.FatalError;
+ }
+
+ var decls = program.TopLevelDeclarations.ToArray();
+ foreach (var decl in decls) {
+ Contract.Assert(decl != null);
+ Bpl.Implementation impl = decl as Bpl.Implementation;
+ if (impl != null && Bpl.CommandLineOptions.Clo.UserWantsToCheckRoutine(impl.Name) && !impl.SkipVerification) {
+ List<Bpl.Counterexample>/*?*/ errors;
+
+ ConditionGeneration.Outcome outcome;
+ int prevAssertionCount = vcgen.CumulativeAssertionCount;
+ try {
+ outcome = vcgen.VerifyImplementation(impl, out errors);
+ } catch (VCGenException) {
+ errors = null;
+ outcome = VCGen.Outcome.Inconclusive;
+ } catch (Bpl.UnexpectedProverOutputException) {
+ errors = null;
+ outcome = VCGen.Outcome.Inconclusive;
+ }
+
+ switch (outcome) {
+ default:
+ Contract.Assert(false); throw new Exception(); // unexpected outcome
+ case VCGen.Outcome.Correct:
+ break;
+ case VCGen.Outcome.TimedOut:
+ er(new DafnyErrorInformation(impl.tok, "Verification timed out (" + impl.Name + ")"));
+ break;
+ case VCGen.Outcome.OutOfMemory:
+ er(new DafnyErrorInformation(impl.tok, "Verification out of memory (" + impl.Name + ")"));
+ break;
+ case VCGen.Outcome.Inconclusive:
+ er(new DafnyErrorInformation(impl.tok, "Verification inconclusive (" + impl.Name + ")"));
+ break;
+ case VCGen.Outcome.Errors:
+ Contract.Assert(errors != null); // guaranteed by postcondition of VerifyImplementation
+
+ errors.Sort(new Bpl.CounterexampleComparer());
+ foreach (var error in errors) {
+ DafnyErrorInformation errorInfo;
+
+ if (error is Bpl.CallCounterexample) {
+ var err = (Bpl.CallCounterexample)error;
+ errorInfo = new DafnyErrorInformation(err.FailingCall.tok, err.FailingCall.ErrorData as string ?? "A precondition for this call might not hold.");
+ errorInfo.AddAuxInfo(err.FailingRequires.tok, err.FailingRequires.ErrorData as string ?? "Related location: This is the precondition that might not hold.");
+
+ } else if (error is Bpl.ReturnCounterexample) {
+ var err = (Bpl.ReturnCounterexample)error;
+ errorInfo = new DafnyErrorInformation(err.FailingReturn.tok, "A postcondition might not hold on this return path.");
+ errorInfo.AddAuxInfo(err.FailingEnsures.tok, err.FailingEnsures.ErrorData as string ?? "Related location: This is the postcondition that might not hold.");
+ errorInfo.AddAuxInfo(err.FailingEnsures.Attributes);
+
+ } else { // error is AssertCounterexample
+ var err = (Bpl.AssertCounterexample)error;
+ if (err.FailingAssert is Bpl.LoopInitAssertCmd) {
+ errorInfo = new DafnyErrorInformation(err.FailingAssert.tok, "This loop invariant might not hold on entry.");
+ } else if (err.FailingAssert is Bpl.LoopInvMaintainedAssertCmd) {
+ // this assertion is a loop invariant which is not maintained
+ errorInfo = new DafnyErrorInformation(err.FailingAssert.tok, "This loop invariant might not be maintained by the loop.");
+ } else {
+ string msg = err.FailingAssert.ErrorData as string;
+ if (msg == null) {
+ msg = "This assertion might not hold.";
+ }
+ errorInfo = new DafnyErrorInformation(err.FailingAssert.tok, msg);
+ errorInfo.AddAuxInfo(err.FailingAssert.Attributes);
+ }
+ }
+ if (Bpl.CommandLineOptions.Clo.ErrorTrace > 0) {
+ foreach (Bpl.Block b in error.Trace) {
+ // for ErrorTrace == 1 restrict the output;
+ // do not print tokens with -17:-4 as their location because they have been
+ // introduced in the translation and do not give any useful feedback to the user
+ if (!(Bpl.CommandLineOptions.Clo.ErrorTrace == 1 && b.tok.line == -17 && b.tok.col == -4) &&
+ b.tok.line != 0 && b.tok.col != 0) {
+ errorInfo.AddAuxInfo(b.tok, "Execution trace: " + b.Label);
+ }
+ }
+ }
+ // if (Bpl.CommandLineOptions.Clo.ModelViewFile != null) {
+ // error.PrintModel();
+ // }
+ er(errorInfo);
+ }
+ break;
+ }
+ }
+ }
+ vcgen.Close();
+ Bpl.CommandLineOptions.Clo.TheProverFactory.Close();
+
+ #endregion
+
+ return PipelineOutcome.VerificationCompleted;
+ }
+
+ public delegate void ErrorReporterDelegate(DafnyErrorInformation errInfo);
+
+ public class DafnyErrorInformation
+ {
+ public readonly Bpl.IToken Tok;
+ public readonly string Msg;
+ public readonly List<DafnyErrorAuxInfo> Aux = new List<DafnyErrorAuxInfo>();
+
+ public class DafnyErrorAuxInfo
+ {
+ public readonly Bpl.IToken Tok;
+ public readonly string Msg;
+ public DafnyErrorAuxInfo(Bpl.IToken tok, string msg) {
+ Tok = tok;
+ Msg = CleanUp(msg);
+ }
+ }
+
+ public DafnyErrorInformation(Bpl.IToken tok, string msg) {
+ Contract.Requires(tok != null);
+ Contract.Requires(1 <= tok.line && 1 <= tok.col);
+ Contract.Requires(msg != null);
+ Tok = tok;
+ Msg = CleanUp(msg);
+ AddNestingsAsAux(tok);
+ }
+ public void AddAuxInfo(Bpl.IToken tok, string msg) {
+ Contract.Requires(tok != null);
+ Contract.Requires(1 <= tok.line && 1 <= tok.col);
+ Contract.Requires(msg != null);
+ Aux.Add(new DafnyErrorAuxInfo(tok, msg));
+ AddNestingsAsAux(tok);
+ }
+ void AddNestingsAsAux(Bpl.IToken tok) {
+ while (tok is Dafny.NestedToken) {
+ var nt = (Dafny.NestedToken)tok;
+ tok = nt.Inner;
+ Aux.Add(new DafnyErrorAuxInfo(tok, "Related location"));
+ }
+ }
+ public void AddAuxInfo(Bpl.QKeyValue attr) {
+ while (attr != null) {
+ if (attr.Key == "msg" && attr.Params.Count == 1 && attr.tok.line != 0 && attr.tok.col != 0) {
+ var str = attr.Params[0] as string;
+ if (str != null) {
+ AddAuxInfo(attr.tok, str);
+ }
+ }
+ attr = attr.Next;
+ }
+ }
+
+ public static string CleanUp(string msg) {
+ if (msg.ToLower().StartsWith("error: ")) {
+ return msg.Substring(7);
+ } else {
+ return msg;
+ }
+ }
+ }
+ }
+}
diff --git a/Source/DafnyExtension/DafnyExtension.csproj b/Source/DafnyExtension/DafnyExtension.csproj new file mode 100644 index 00000000..2580c396 --- /dev/null +++ b/Source/DafnyExtension/DafnyExtension.csproj @@ -0,0 +1,191 @@ +<?xml version="1.0" encoding="utf-8"?>
+<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
+ <Import Project="$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props" Condition="Exists('$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props')" />
+ <PropertyGroup>
+ <Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
+ <Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
+ <ProductVersion>10.0.20305</ProductVersion>
+ <SchemaVersion>2.0</SchemaVersion>
+ <ProjectTypeGuids>{82b43b9b-a64c-4715-b499-d71e9ca2bd60};{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}</ProjectTypeGuids>
+ <ProjectGuid>{6E9A5E14-0763-471C-A129-80A879D9E7BA}</ProjectGuid>
+ <OutputType>Library</OutputType>
+ <AppDesignerFolder>Properties</AppDesignerFolder>
+ <RootNamespace>DafnyLanguage</RootNamespace>
+ <AssemblyName>DafnyLanguageService</AssemblyName>
+ <TargetFrameworkVersion>v4.0</TargetFrameworkVersion>
+ <FileAlignment>512</FileAlignment>
+ <GeneratePkgDefFile>false</GeneratePkgDefFile>
+ <MinimumVisualStudioVersion>11.0</MinimumVisualStudioVersion>
+ <FileUpgradeFlags>
+ </FileUpgradeFlags>
+ <UpgradeBackupLocation>
+ </UpgradeBackupLocation>
+ <OldToolsVersion>4.0</OldToolsVersion>
+ </PropertyGroup>
+ <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
+ <DebugSymbols>true</DebugSymbols>
+ <DebugType>full</DebugType>
+ <Optimize>false</Optimize>
+ <OutputPath>bin\Debug\</OutputPath>
+ <DefineConstants>DEBUG;TRACE</DefineConstants>
+ <ErrorReport>prompt</ErrorReport>
+ <WarningLevel>4</WarningLevel>
+ </PropertyGroup>
+ <PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
+ <DebugType>pdbonly</DebugType>
+ <Optimize>true</Optimize>
+ <OutputPath>bin\Release\</OutputPath>
+ <DefineConstants>TRACE</DefineConstants>
+ <ErrorReport>prompt</ErrorReport>
+ <WarningLevel>4</WarningLevel>
+ </PropertyGroup>
+ <ItemGroup>
+ <Reference Include="AbsInt, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
+ <SpecificVersion>False</SpecificVersion>
+ <HintPath>..\..\..\..\Binaries\AbsInt.dll</HintPath>
+ </Reference>
+ <Reference Include="AIFramework, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
+ <SpecificVersion>False</SpecificVersion>
+ <HintPath>..\..\..\..\Binaries\AIFramework.dll</HintPath>
+ </Reference>
+ <Reference Include="Basetypes, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
+ <SpecificVersion>False</SpecificVersion>
+ <HintPath>..\..\..\..\Binaries\Basetypes.dll</HintPath>
+ </Reference>
+ <Reference Include="CodeContractsExtender, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
+ <SpecificVersion>False</SpecificVersion>
+ <HintPath>..\..\..\..\Binaries\CodeContractsExtender.dll</HintPath>
+ </Reference>
+ <Reference Include="Core, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
+ <SpecificVersion>False</SpecificVersion>
+ <HintPath>..\..\..\..\Binaries\Core.dll</HintPath>
+ </Reference>
+ <Reference Include="DafnyPipeline, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
+ <SpecificVersion>False</SpecificVersion>
+ <HintPath>..\..\..\..\Binaries\DafnyPipeline.dll</HintPath>
+ </Reference>
+ <Reference Include="Graph">
+ <HintPath>..\..\..\..\Binaries\Graph.dll</HintPath>
+ </Reference>
+ <Reference Include="Houdini">
+ <HintPath>..\..\..\..\Binaries\Houdini.dll</HintPath>
+ </Reference>
+ <Reference Include="Model">
+ <HintPath>..\..\..\..\Binaries\Model.dll</HintPath>
+ </Reference>
+ <Reference Include="ParserHelper">
+ <HintPath>..\..\..\..\Binaries\ParserHelper.dll</HintPath>
+ </Reference>
+ <Reference Include="Provers.Z3">
+ <HintPath>..\..\..\..\Binaries\Provers.Z3.dll</HintPath>
+ </Reference>
+ <Reference Include="Provers.SMTLib">
+ <HintPath>..\..\..\..\Binaries\Provers.SMTLib.dll</HintPath>
+ </Reference>
+ <Reference Include="VCExpr">
+ <HintPath>..\..\..\..\Binaries\VCExpr.dll</HintPath>
+ </Reference>
+ <Reference Include="VCGeneration, Version=2.0.0.0, Culture=neutral, PublicKeyToken=736440c9b414ea16, processorArchitecture=MSIL">
+ <SpecificVersion>False</SpecificVersion>
+ <HintPath>..\..\..\..\Binaries\VCGeneration.dll</HintPath>
+ </Reference>
+ <Reference Include="EnvDTE, Version=8.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a">
+ <EmbedInteropTypes>False</EmbedInteropTypes>
+ </Reference>
+ <Reference Include="Microsoft.VisualStudio.CoreUtility">
+ <Private>False</Private>
+ </Reference>
+ <Reference Include="Microsoft.VisualStudio.Editor, Version=10.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />
+ <Reference Include="Microsoft.VisualStudio.Language.Intellisense, Version=10.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />
+ <Reference Include="Microsoft.VisualStudio.Language.StandardClassification, Version=10.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />
+ <Reference Include="Microsoft.VisualStudio.OLE.Interop, Version=7.1.40304.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a" />
+ <Reference Include="Microsoft.VisualStudio.Shell, Version=2.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">
+ <Private>False</Private>
+ </Reference>
+ <Reference Include="Microsoft.VisualStudio.Shell.Immutable.10.0, Version=10.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL" />
+ <Reference Include="Microsoft.VisualStudio.Shell.Interop, Version=7.1.40304.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a" />
+ <Reference Include="Microsoft.VisualStudio.Shell.Interop.10.0, Version=10.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">
+ <EmbedInteropTypes>True</EmbedInteropTypes>
+ </Reference>
+ <Reference Include="Microsoft.VisualStudio.Shell.Interop.8.0, Version=8.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a" />
+ <Reference Include="Microsoft.VisualStudio.Text.Data">
+ <Private>False</Private>
+ </Reference>
+ <Reference Include="Microsoft.VisualStudio.Text.Logic">
+ <Private>False</Private>
+ </Reference>
+ <Reference Include="Microsoft.VisualStudio.Text.UI">
+ <Private>False</Private>
+ </Reference>
+ <Reference Include="Microsoft.VisualStudio.Text.UI.Wpf">
+ <Private>False</Private>
+ </Reference>
+ <Reference Include="Microsoft.VisualStudio.TextManager.Interop, Version=7.1.40304.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a" />
+ <Reference Include="PresentationCore" />
+ <Reference Include="PresentationFramework" />
+ <Reference Include="System" />
+ <Reference Include="Microsoft.CSharp" />
+ <Reference Include="System.ComponentModel.Composition" />
+ <Reference Include="System.Core" />
+ <Reference Include="System.Data.DataSetExtensions" />
+ <Reference Include="System.Data" />
+ <Reference Include="System.Xml" />
+ <Reference Include="System.Xaml" />
+ <Reference Include="WindowsBase" />
+ </ItemGroup>
+ <ItemGroup>
+ <Compile Include="BufferIdleEventUtil.cs" />
+ <Compile Include="HoverText.cs" />
+ <Compile Include="IdentifierTagger.cs" />
+ <Compile Include="ProgressMargin.cs" />
+ <Compile Include="OutliningTagger.cs" />
+ <Compile Include="ResolverTagger.cs" />
+ <Compile Include="DafnyDriver.cs" />
+ <Compile Include="ContentType.cs" />
+ <Compile Include="BraceMatching.cs" />
+ <Compile Include="WordHighlighter.cs" />
+ <Compile Include="ErrorTagger.cs" />
+ <Compile Include="TokenTagger.cs" />
+ <Compile Include="ClassificationTagger.cs" />
+ <Compile Include="Properties\AssemblyInfo.cs" />
+ </ItemGroup>
+ <ItemGroup>
+ <Content Include="DafnyPrelude.bpl">
+ <IncludeInVSIX>true</IncludeInVSIX>
+ <CopyToOutputDirectory>Always</CopyToOutputDirectory>
+ </Content>
+ <None Include="source.extension.vsixmanifest">
+ <SubType>Designer</SubType>
+ </None>
+ <Content Include="UnivBackPred2.smt2">
+ <IncludeInVSIX>true</IncludeInVSIX>
+ <CopyToOutputDirectory>Always</CopyToOutputDirectory>
+ </Content>
+ </ItemGroup>
+ <ItemGroup>
+ <WCFMetadata Include="Service References\" />
+ </ItemGroup>
+ <PropertyGroup>
+ <VisualStudioVersion Condition="'$(VisualStudioVersion)' == ''">10.0</VisualStudioVersion>
+ <VSToolsPath Condition="'$(VSToolsPath)' == ''">$(MSBuildExtensionsPath32)\Microsoft\VisualStudio\v$(VisualStudioVersion)</VSToolsPath>
+ </PropertyGroup>
+ <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />
+ <Import Project="$(VSToolsPath)\VSSDK\Microsoft.VsSDK.targets" Condition="'$(VSToolsPath)' != ''" />
+ <Import Project="$(MSBuildExtensionsPath32)\Microsoft\VisualStudio\v10.0\VSSDK\Microsoft.VsSDK.targets" Condition="false" />
+ <PropertyGroup>
+ <PostBuildEvent>cd</PostBuildEvent>
+ <PostBuildEvent>
+ </PostBuildEvent>
+ </PropertyGroup>
+ <PropertyGroup>
+ <PreBuildEvent>copy ..\..\..\..\..\..\Binaries\DafnyPrelude.bpl $(ProjectDir)
+copy ..\..\..\..\..\..\Binaries\UnivBackPred2.smt2 $(ProjectDir)</PreBuildEvent>
+ </PropertyGroup>
+ <!-- To modify your build process, add your task inside one of the targets below and uncomment it.
+ Other similar extension points exist, see Microsoft.Common.targets.
+ <Target Name="BeforeBuild">
+ </Target>
+ <Target Name="AfterBuild">
+ </Target>
+ -->
+</Project>
\ No newline at end of file diff --git a/Source/DafnyExtension/ErrorTagger.cs b/Source/DafnyExtension/ErrorTagger.cs new file mode 100644 index 00000000..efd755d8 --- /dev/null +++ b/Source/DafnyExtension/ErrorTagger.cs @@ -0,0 +1,85 @@ +//***************************************************************************
+// 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;
+
+namespace DafnyLanguage
+{
+ [Export(typeof(ITaggerProvider))]
+ [ContentType("dafny")]
+ [TagType(typeof(ErrorTag))]
+ internal sealed class ErrorTaggerProvider : 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 ErrorTagger(buffer, tagAggregator) as ITagger<T>; };
+ return buffer.Properties.GetOrCreateSingletonProperty<ITagger<T>>(sc);
+ }
+ }
+
+ /// <summary>
+ /// Translate PkgDefTokenTags into ErrorTags and Error List items
+ /// </summary>
+ internal sealed class ErrorTagger : ITagger<ErrorTag>
+ {
+ ITextBuffer _buffer;
+ ITagAggregator<DafnyResolverTag> _aggregator;
+
+ internal ErrorTagger(ITextBuffer buffer, ITagAggregator<DafnyResolverTag> tagAggregator) {
+ _buffer = buffer;
+ _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<ErrorTag>> GetTags(NormalizedSnapshotSpanCollection spans) {
+ if (spans.Count == 0) yield break;
+ var snapshot = spans[0].Snapshot;
+ foreach (var tagSpan in this._aggregator.GetTags(spans)) {
+ DafnyResolverTag t = tagSpan.Tag;
+ DafnyErrorResolverTag et = t as DafnyErrorResolverTag;
+ if (et != null) {
+ foreach (SnapshotSpan s in tagSpan.Span.GetSpans(snapshot)) {
+ yield return new TagSpan<ErrorTag>(s, new ErrorTag(et.Typ, et.Msg));
+ }
+ }
+ }
+ }
+
+ // 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 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));
+ }
+ }
+ }
+ }
+}
diff --git a/Source/DafnyExtension/HoverText.cs b/Source/DafnyExtension/HoverText.cs new file mode 100644 index 00000000..be806f5b --- /dev/null +++ b/Source/DafnyExtension/HoverText.cs @@ -0,0 +1,126 @@ +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 DafnyQuickInfoSource(textBuffer, aggService.CreateTagAggregator<DafnyTokenTag>(textBuffer));
+ }
+ }
+
+ class DafnyQuickInfoSource : IQuickInfoSource
+ {
+ private ITagAggregator<DafnyTokenTag> _aggregator;
+ private ITextBuffer _buffer;
+
+ public DafnyQuickInfoSource(ITextBuffer buffer, ITagAggregator<DafnyTokenTag> aggregator) {
+ _aggregator = aggregator;
+ _buffer = buffer;
+ }
+
+ public void AugmentQuickInfoSession(IQuickInfoSession session, IList<object> quickInfoContent, out ITrackingSpan applicableToSpan) {
+ applicableToSpan = null;
+
+ var triggerPoint = (SnapshotPoint)session.GetTriggerPoint(_buffer.CurrentSnapshot);
+ if (triggerPoint == null)
+ return;
+
+ foreach (IMappingTagSpan<DafnyTokenTag> 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() {
+ }
+ }
+ // --------------------------------- 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<ITextBuffer> subjectBuffers) {
+ return new DafnyQuickInfoController(textView, subjectBuffers, this);
+ }
+ }
+
+ class DafnyQuickInfoController : IIntellisenseController
+ {
+ private ITextView _textView;
+ private IList<ITextBuffer> _subjectBuffers;
+ private DafnyQuickInfoControllerProvider _componentContext;
+
+ private IQuickInfoSession _session;
+
+ internal DafnyQuickInfoController(ITextView textView, IList<ITextBuffer> 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/Source/DafnyExtension/IdentifierTagger.cs b/Source/DafnyExtension/IdentifierTagger.cs new file mode 100644 index 00000000..5ecc8dc2 --- /dev/null +++ b/Source/DafnyExtension/IdentifierTagger.cs @@ -0,0 +1,344 @@ +//***************************************************************************
+// 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 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
+ Microsoft.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) {
+ DafnyTokenKinds kind;
+ switch (r.Kind) {
+ case IdRegion.OccurrenceKind.Use:
+ kind = DafnyTokenKinds.VariableIdentifier; break;
+ case IdRegion.OccurrenceKind.Definition:
+ kind = DafnyTokenKinds.VariableIdentifierDefinition; break;
+ case IdRegion.OccurrenceKind.WildDefinition:
+ kind = DafnyTokenKinds.Keyword; break;
+ default:
+ Contract.Assert(false); // unexpected OccurrenceKind
+ goto case IdRegion.OccurrenceKind.Use; // to please compiler
+ }
+ yield return new TagSpan<DafnyTokenTag>(
+ new SnapshotSpan(_snapshot, r.Start, r.Length),
+ new DafnyTokenTag(kind, 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) {
+ ITextSnapshot snap;
+ Microsoft.Dafny.Program prog;
+ lock (this) {
+ snap = r._snapshot;
+ prog = r._program;
+ }
+ if (prog != null) {
+ if (!ComputeIdentifierRegions(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));
+ }
+ }
+ }
+ }
+ }
+
+ bool ComputeIdentifierRegions(Microsoft.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 (var d in module.TopLevelDecls) {
+ if (d is DatatypeDecl) {
+ var dt = (DatatypeDecl)d;
+ foreach (var ctor in dt.Ctors) {
+ foreach (var dtor in ctor.Destructors) {
+ if (dtor != null) {
+ IdRegion.Add(newRegions, dtor.tok, dtor, null, "destructor", true, module);
+ }
+ }
+ }
+ } else if (d is ClassDecl) {
+ var cl = (ClassDecl)d;
+ foreach (var member in cl.Members) {
+ if (member is Function) {
+ var f = (Function)member;
+ foreach (var p in f.Formals) {
+ IdRegion.Add(newRegions, p.tok, p, true, module);
+ }
+ f.Req.ForEach(e => ExprRegions(e, newRegions, module));
+ f.Reads.ForEach(fe => FrameExprRegions(fe, newRegions, true, module));
+ f.Ens.ForEach(e => ExprRegions(e, newRegions, module));
+ f.Decreases.Expressions.ForEach(e => ExprRegions(e, newRegions, module));
+ if (f.Body != null) {
+ ExprRegions(f.Body, newRegions, module);
+ }
+ } else if (member is Method) {
+ var m = (Method)member;
+ foreach (var p in m.Ins) {
+ IdRegion.Add(newRegions, p.tok, p, true, module);
+ }
+ foreach (var p in m.Outs) {
+ IdRegion.Add(newRegions, p.tok, p, true, module);
+ }
+ m.Req.ForEach(e => ExprRegions(e.E, newRegions, module));
+ m.Mod.Expressions.ForEach(fe => FrameExprRegions(fe, newRegions, true, module));
+ m.Ens.ForEach(e => ExprRegions(e.E, newRegions, module));
+ m.Decreases.Expressions.ForEach(e => ExprRegions(e, newRegions, module));
+ if (m.Body != null) {
+ StatementRegions(m.Body, newRegions, module);
+ }
+ } else if (member is Field) {
+ var fld = (Field)member;
+ IdRegion.Add(newRegions, fld.tok, fld, null, "field", true, module);
+ }
+ }
+ }
+ }
+ }
+ _snapshot = snapshot;
+ _regions = newRegions;
+ _program = program;
+ return true;
+ }
+
+ static void FrameExprRegions(FrameExpression fe, List<IdRegion> regions, bool descendIntoExpressions, ModuleDefinition module) {
+ Contract.Requires(fe != null);
+ Contract.Requires(regions != null);
+ if (descendIntoExpressions) {
+ ExprRegions(fe.E, regions, module);
+ }
+ if (fe.Field != null) {
+ Microsoft.Dafny.Type showType = null; // TODO: if we had the instantiated type of this field, that would have been nice to use here (but the Resolver currently does not compute or store the instantiated type for a FrameExpression)
+ IdRegion.Add(regions, fe.tok, fe.Field, showType, "field", false, module);
+ }
+ }
+
+ static void ExprRegions(Microsoft.Dafny.Expression expr, List<IdRegion> regions, ModuleDefinition module) {
+ Contract.Requires(expr != null);
+ Contract.Requires(regions != null);
+ if (expr is IdentifierExpr) {
+ var e = (IdentifierExpr)expr;
+ IdRegion.Add(regions, e.tok, e.Var, false, module);
+ } else if (expr is FieldSelectExpr) {
+ var e = (FieldSelectExpr)expr;
+ IdRegion.Add(regions, e.tok, e.Field, e.Type, "field", false, module);
+ } else if (expr is ComprehensionExpr) {
+ var e = (ComprehensionExpr)expr;
+ foreach (var bv in e.BoundVars) {
+ IdRegion.Add(regions, bv.tok, bv, true, module);
+ }
+ } else if (expr is MatchExpr) {
+ var e = (MatchExpr)expr;
+ foreach (var kase in e.Cases) {
+ kase.Arguments.ForEach(bv => IdRegion.Add(regions, bv.tok, bv, true, module));
+ }
+ } else if (expr is ChainingExpression) {
+ var e = (ChainingExpression)expr;
+ // Do the subexpressions only once (that is, avoid the duplication that occurs in the desugared form of the ChainingExpression)
+ e.Operands.ForEach(ee => ExprRegions(ee, regions, module));
+ return; // return here, so as to avoid doing the subexpressions below
+ }
+ foreach (var ee in expr.SubExpressions) {
+ ExprRegions(ee, regions, module);
+ }
+ }
+
+ static void StatementRegions(Statement stmt, List<IdRegion> regions, ModuleDefinition module) {
+ Contract.Requires(stmt != null);
+ Contract.Requires(regions != null);
+ if (stmt is VarDeclStmt) {
+ var s = (VarDeclStmt)stmt;
+ // Add the variables here, once, and then go directly to the RHS's (without letting the sub-statements re-do the LHS's)
+ foreach (var lhs in s.Lhss) {
+ IdRegion.Add(regions, lhs.Tok, lhs, true, module);
+ }
+ if (s.Update == null) {
+ // the VarDeclStmt has no associated assignment
+ } else if (s.Update is UpdateStmt) {
+ var upd = (UpdateStmt)s.Update;
+ foreach (var rhs in upd.Rhss) {
+ foreach (var ee in rhs.SubExpressions) {
+ ExprRegions(ee, regions, module);
+ }
+ }
+ } else {
+ var upd = (AssignSuchThatStmt)s.Update;
+ ExprRegions(upd.Expr, regions, module);
+ }
+ // we're done, so don't do the sub-statements/expressions again
+ return;
+ } else if (stmt is VarDecl) {
+ var s = (VarDecl)stmt;
+ IdRegion.Add(regions, s.Tok, s, true, module);
+ } else if (stmt is ParallelStmt) {
+ var s = (ParallelStmt)stmt;
+ s.BoundVars.ForEach(bv => IdRegion.Add(regions, bv.tok, bv, true, module));
+ } else if (stmt is MatchStmt) {
+ var s = (MatchStmt)stmt;
+ foreach (var kase in s.Cases) {
+ kase.Arguments.ForEach(bv => IdRegion.Add(regions, bv.tok, bv, true, module));
+ }
+ } else if (stmt is LoopStmt) {
+ var s = (LoopStmt)stmt;
+ if (s.Mod.Expressions != null) {
+ s.Mod.Expressions.ForEach(fe => FrameExprRegions(fe, regions, false, module));
+ }
+ }
+ foreach (var ee in stmt.SubExpressions) {
+ ExprRegions(ee, regions, module);
+ }
+ foreach (var ss in stmt.SubStatements) {
+ StatementRegions(ss, regions, module);
+ }
+ }
+
+ class IdRegion
+ {
+ public readonly int Start;
+ public readonly int Length;
+ public readonly string HoverText;
+ public enum OccurrenceKind { Use, Definition, WildDefinition }
+ public readonly OccurrenceKind Kind;
+
+ static bool SurfaceSyntaxToken(Bpl.IToken tok) {
+ Contract.Requires(tok != null);
+ return !(tok is TokenWrapper);
+ }
+
+ public static void Add(List<IdRegion> regions, Bpl.IToken tok, IVariable v, bool isDefinition, ModuleDefinition context) {
+ Contract.Requires(regions != null);
+ Contract.Requires(tok != null);
+ Contract.Requires(v != null);
+ if (SurfaceSyntaxToken(tok)) {
+ regions.Add(new IdRegion(tok, v, isDefinition, context));
+ }
+ }
+ public static void Add(List<IdRegion> regions, Bpl.IToken tok, Field decl, Microsoft.Dafny.Type showType, string kind, bool isDefinition, ModuleDefinition context) {
+ Contract.Requires(regions != null);
+ Contract.Requires(tok != null);
+ Contract.Requires(decl != null);
+ Contract.Requires(kind != null);
+ if (SurfaceSyntaxToken(tok)) {
+ regions.Add(new IdRegion(tok, decl, showType, kind, isDefinition, context));
+ }
+ }
+
+ private IdRegion(Bpl.IToken tok, IVariable v, bool isDefinition, ModuleDefinition context) {
+ Contract.Requires(tok != null);
+ Contract.Requires(v != null);
+ Start = tok.pos;
+ Length = v.DisplayName.Length;
+ string kind;
+ if (v is VarDecl) {
+ kind = "local variable";
+ } else if (v is BoundVar) {
+ kind = "bound variable";
+ } else {
+ var formal = (Formal)v;
+ kind = formal.InParam ? "in-parameter" : "out-parameter";
+ }
+ HoverText = string.Format("({2}{3}) {0}: {1}", v.DisplayName, v.Type.TypeName(context), v.IsGhost ? "ghost " : "", kind);
+ Kind = !isDefinition ? OccurrenceKind.Use : VarDecl.HasWildcardName(v) ? OccurrenceKind.WildDefinition : OccurrenceKind.Definition;
+ }
+ private IdRegion(Bpl.IToken tok, Field decl, Microsoft.Dafny.Type showType, string kind, bool isDefinition, ModuleDefinition context) {
+ Contract.Requires(tok != null);
+ Contract.Requires(decl != null);
+ Contract.Requires(kind != null);
+ if (showType == null) {
+ showType = decl.Type;
+ }
+ Start = tok.pos;
+ Length = decl.Name.Length;
+ HoverText = string.Format("({2}{3}) {0}: {1}", decl.FullNameInContext(context), showType.TypeName(context), decl.IsGhost ? "ghost " : "", kind);
+ Kind = !isDefinition ? OccurrenceKind.Use : OccurrenceKind.Definition;
+ }
+ }
+ }
+
+}
diff --git a/Source/DafnyExtension/OutliningTagger.cs b/Source/DafnyExtension/OutliningTagger.cs new file mode 100644 index 00000000..a47cdba7 --- /dev/null +++ b/Source/DafnyExtension/OutliningTagger.cs @@ -0,0 +1,185 @@ +//***************************************************************************
+// 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(IOutliningRegionTag))]
+ internal sealed class OutliningTaggerProvider : 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 OutliningTagger(buffer, tagAggregator) as ITagger<T>; };
+ return buffer.Properties.GetOrCreateSingletonProperty<ITagger<T>>(sc);
+ }
+ }
+
+ /// <summary>
+ /// Translate DafnyResolverTag's into IOutliningRegionTag's
+ /// </summary>
+ internal sealed class OutliningTagger : ITagger<IOutliningRegionTag>
+ {
+ 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<ORegion> _regions = new List<ORegion>(); // the regions generated from _program
+ ITagAggregator<DafnyResolverTag> _aggregator;
+
+ internal OutliningTagger(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<IOutliningRegionTag>> 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;
+ if (start == end) yield break;
+
+ foreach (var r in _regions) {
+ if (0 <= r.Length && r.Start <= end && start <= r.Start + r.Length) {
+ yield return new TagSpan<OutliningRegionTag>(
+ new SnapshotSpan(_snapshot, r.Start, r.Length),
+ new OutliningRegionTag(false, false, "...", 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) {
+ 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));
+ }
+ }
+ }
+ }
+ }
+
+ bool ComputeOutliningRegions(Dafny.Program program, ITextSnapshot snapshot) {
+ Contract.Requires(snapshot != null);
+
+ if (program == _program)
+ return false; // no new regions
+
+ List<ORegion> newRegions = new List<ORegion>();
+
+ foreach (var module in program.Modules) {
+ if (!module.IsDefaultModule) {
+ newRegions.Add(new ORegion(module, "module"));
+ }
+ foreach (Dafny.TopLevelDecl d in module.TopLevelDecls) {
+ if (!HasBodyTokens(d) && !(d is Dafny.ClassDecl)) {
+ continue;
+ }
+ if (d is Dafny.ArbitraryTypeDecl) {
+ newRegions.Add(new ORegion(d, "type"));
+ } else if (d is Dafny.CoDatatypeDecl) {
+ newRegions.Add(new ORegion(d, "codatatype"));
+ } else if (d is Dafny.DatatypeDecl) {
+ newRegions.Add(new ORegion(d, "datatype"));
+ } else if (d is Dafny.ModuleDecl) {
+ // do nothing here, since the outer loop handles modules
+ } else {
+ Dafny.ClassDecl cl = (Dafny.ClassDecl)d;
+ if (!cl.IsDefaultClass) {
+ newRegions.Add(new ORegion(cl, "class"));
+ }
+ // do the class members (in particular, functions and methods)
+ foreach (Dafny.MemberDecl m in cl.Members) {
+ if (!HasBodyTokens(m)) {
+ continue;
+ }
+ if (m is Dafny.Function && ((Dafny.Function)m).Body != null) {
+ newRegions.Add(new ORegion(m, m is Dafny.CoPredicate ? "copredicate" : m is Dafny.Predicate ? "predicate" : "function"));
+ } else if (m is Dafny.Method && ((Dafny.Method)m).Body != null) {
+ newRegions.Add(new ORegion(m, m is Dafny.Constructor ? "constructor" : "method"));
+ }
+ }
+ }
+ }
+ }
+ _snapshot = snapshot;
+ _regions = newRegions;
+ _program = program;
+ return true;
+ }
+
+ bool HasBodyTokens(Dafny.Declaration decl) {
+ Contract.Requires(decl != null);
+ return decl.BodyStartTok != Bpl.Token.NoToken && decl.BodyEndTok != Bpl.Token.NoToken;
+ }
+
+ class ORegion
+ {
+ public readonly int Start;
+ public readonly int Length;
+ public readonly string HoverText;
+ public ORegion(Dafny.Declaration decl, string kind) {
+ int startPosition = decl.BodyStartTok.pos + 1; // skip the open-curly brace itself
+ int length = decl.BodyEndTok.pos - startPosition;
+ Start = startPosition;
+ Length = length;
+ HoverText = string.Format("body of {0} {1}", kind, decl.Name);
+ }
+ }
+ }
+}
diff --git a/Source/DafnyExtension/ProgressMargin.cs b/Source/DafnyExtension/ProgressMargin.cs new file mode 100644 index 00000000..7fdf38a6 --- /dev/null +++ b/Source/DafnyExtension/ProgressMargin.cs @@ -0,0 +1,260 @@ +using System;
+using System.Collections.Generic;
+using System.Threading;
+using System.Windows.Threading;
+using System.Windows;
+using System.Windows.Shapes;
+using System.Windows.Media;
+using System.Windows.Controls;
+using System.ComponentModel.Composition;
+using Microsoft.VisualStudio.Text;
+using Microsoft.VisualStudio.Text.Editor;
+using Microsoft.VisualStudio.Text.Formatting;
+using Microsoft.VisualStudio.Text.Tagging;
+using Microsoft.VisualStudio.Text.Classification;
+using Microsoft.VisualStudio.Shell;
+using Microsoft.VisualStudio.Utilities;
+using System.Diagnostics.Contracts;
+using Dafny = Microsoft.Dafny;
+using Bpl = Microsoft.Boogie;
+
+
+namespace DafnyLanguage
+{
+ #region UI stuff
+ internal class ProgressMarginGlyphFactory : IGlyphFactory
+ {
+ public UIElement GenerateGlyph(IWpfTextViewLine line, IGlyphTag tag) {
+ var dtag = tag as ProgressGlyphTag;
+ if (dtag == null) {
+ return null;
+ }
+
+ System.Windows.Shapes.Rectangle sh = new Rectangle() {
+ Fill = dtag.Val == 0 ? Brushes.Violet : Brushes.DarkOrange,
+ Height = 18.0,
+ Width = 3.0
+ };
+ return sh;
+ }
+ }
+
+ [Export(typeof(IGlyphFactoryProvider))]
+ [Name("ProgressMarginGlyph")]
+ [Order(After = "TokenTagger")]
+ [ContentType("dafny")]
+ [TagType(typeof(ProgressGlyphTag))]
+ internal sealed class ProgressMarginGlyphFactoryProvider : IGlyphFactoryProvider
+ {
+ public IGlyphFactory GetGlyphFactory(IWpfTextView view, IWpfTextViewMargin margin) {
+ return new ProgressMarginGlyphFactory();
+ }
+ }
+
+ internal class ProgressGlyphTag : IGlyphTag
+ {
+ public readonly int Val;
+ public ProgressGlyphTag(int val) {
+ Val = val;
+ }
+ }
+ #endregion
+
+ [Export(typeof(ITaggerProvider))]
+ [ContentType("dafny")]
+ [TagType(typeof(ProgressGlyphTag))]
+ class ProgressTaggerProvider : ITaggerProvider
+ {
+ [Import]
+ internal IBufferTagAggregatorFactoryService AggregatorFactory = null;
+
+ [Import(typeof(Microsoft.VisualStudio.Shell.SVsServiceProvider))]
+ internal IServiceProvider _serviceProvider = 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 ProgressTagger(buffer, _serviceProvider, tagAggregator) as ITagger<T>; };
+ return buffer.Properties.GetOrCreateSingletonProperty<ITagger<T>>(sc);
+ }
+ }
+
+ internal class ProgressTagger : ITagger<ProgressGlyphTag>
+ {
+ ErrorListProvider _errorProvider;
+ ITextBuffer _buffer;
+
+ readonly DispatcherTimer timer;
+
+ public ProgressTagger(ITextBuffer buffer, IServiceProvider serviceProvider, ITagAggregator<DafnyResolverTag> tagAggregator) {
+ _buffer = buffer;
+ _errorProvider = new ErrorListProvider(serviceProvider);
+
+ timer = new DispatcherTimer(DispatcherPriority.ApplicationIdle);
+ timer.Interval = TimeSpan.FromMilliseconds(500);
+ timer.Tick += new EventHandler(UponIdle);
+
+ tagAggregator.TagsChanged += new EventHandler<TagsChangedEventArgs>(_aggregator_TagsChanged);
+ buffer.Changed += new EventHandler<TextContentChangedEventArgs>(buffer_Changed);
+ bufferChangesPostVerificationStart.Add(new SnapshotSpan(buffer.CurrentSnapshot, 0, buffer.CurrentSnapshot.Length));
+ }
+
+ public void Dispose() {
+ }
+
+ // The following fields and the contents of the following two lists are protected by the lock "this".
+ List<SnapshotSpan> bufferChangesPreVerificationStart = new List<SnapshotSpan>(); // buffer changes after the last completed verification and before the currently running verification
+ List<SnapshotSpan> bufferChangesPostVerificationStart = new List<SnapshotSpan>(); // buffer changes since the start of the currently running verification
+
+ void buffer_Changed(object sender, TextContentChangedEventArgs e) {
+ lock (this) {
+ foreach (var change in e.Changes) {
+ var startLine = e.After.GetLineFromPosition(change.NewPosition);
+ var endLine = e.After.GetLineFromPosition(change.NewEnd);
+ bufferChangesPostVerificationStart.Add(new SnapshotSpan(startLine.Start, endLine.End));
+ }
+ }
+ }
+
+ // The next field is protected by "this"
+ ResolverTagger resolver;
+ // Keep track of the most recent resolution results.
+ void _aggregator_TagsChanged(object sender, TagsChangedEventArgs e) {
+ var r = sender as ResolverTagger;
+ if (r != null) {
+ lock (this) {
+ resolver = r;
+ }
+ timer.Stop();
+ timer.Start();
+ }
+ }
+
+ bool verificationInProgress; // this field is protected by "this". Invariant: !verificationInProgress ==> bufferChangesPreVerificationStart.Count == 0
+ /// <summary>
+ /// This method is invoked when the user has been idle for a little while.
+ /// Note, "sender" and "args" are allowed to be passed in as null--they are not used by this method.
+ /// </summary>
+ public void UponIdle(object sender, EventArgs args) {
+ Dafny.Program prog;
+ ITextSnapshot snap;
+ ResolverTagger r;
+ lock (this) {
+ if (verificationInProgress) {
+ // This UponIdle message came at an inopportune time--we've already kicked off a verification.
+ // Just back off.
+ return;
+ }
+
+ if (resolver == null) return;
+ lock (resolver) {
+ prog = resolver._program;
+ snap = resolver._snapshot;
+ }
+ r = resolver;
+ resolver = null;
+ if (prog == null) return;
+ // We have a successfully resolved program to verify
+
+ var resolvedVersion = snap.Version.VersionNumber;
+ if (bufferChangesPostVerificationStart.Count == 0) {
+ // Nothing new to verify. No reason to start a new verification.
+ return;
+ } else if (!bufferChangesPostVerificationStart.TrueForAll(span => span.Snapshot.Version.VersionNumber <= resolvedVersion)) {
+ // There have been buffer changes since the program that was resolved. Do nothing here,
+ // and instead just await the next resolved program.
+ return;
+ }
+
+ // at this time, we're committed to running the verifier
+ verificationInProgress = true;
+
+ // Change orange progress markers into yellow ones
+ Contract.Assert(bufferChangesPreVerificationStart.Count == 0); // follows from monitor invariant
+ var empty = bufferChangesPreVerificationStart;
+ bufferChangesPreVerificationStart = bufferChangesPostVerificationStart;
+ bufferChangesPostVerificationStart = empty;
+ // Notify to-whom-it-may-concern about the changes we just made
+ var chng = TagsChanged;
+ if (chng != null) {
+ chng(this, new SnapshotSpanEventArgs(new SnapshotSpan(snap, 0, snap.Length)));
+ }
+
+ }
+ new Thread(() => VerificationWorker(prog, snap, r)).Start();
+ }
+
+ /// <summary>
+ /// Thread entry point.
+ /// </summary>
+ void VerificationWorker(Dafny.Program program, ITextSnapshot snapshot, ResolverTagger errorListHolder) {
+ Contract.Requires(program != null);
+ Contract.Requires(snapshot != null);
+ Contract.Requires(errorListHolder != null);
+
+ // Run the verifier
+ var newErrors = new List<DafnyError>();
+ try {
+ bool success = DafnyDriver.Verify(program, errorInfo => {
+ newErrors.Add(new DafnyError(errorInfo.Tok.line - 1, errorInfo.Tok.col - 1, ErrorCategory.VerificationError, errorInfo.Msg));
+ foreach (var aux in errorInfo.Aux) {
+ newErrors.Add(new DafnyError(aux.Tok.line - 1, aux.Tok.col - 1, ErrorCategory.AuxInformation, aux.Msg));
+ }
+ });
+ if (!success) {
+ newErrors.Add(new DafnyError(0, 0, ErrorCategory.InternalError, "verification process error"));
+ }
+ } catch (Exception e) {
+ newErrors.Add(new DafnyError(0, 0, ErrorCategory.InternalError, "verification process error: " + e.Message));
+ }
+ errorListHolder.PopulateErrorList(newErrors, true, snapshot);
+
+ lock (this) {
+ bufferChangesPreVerificationStart.Clear();
+ verificationInProgress = false;
+ }
+ // Notify to-whom-it-may-concern about the cleared pre-verification changes
+ var chng = TagsChanged;
+ if (chng != null) {
+ chng(this, new SnapshotSpanEventArgs(new SnapshotSpan(snapshot, 0, snapshot.Length)));
+ }
+
+ // If new changes took place since we started the verification, we may need to kick off another verification
+ // immediately.
+ UponIdle(null, null);
+ }
+
+ public event EventHandler<SnapshotSpanEventArgs> TagsChanged;
+ IEnumerable<ITagSpan<ProgressGlyphTag>> ITagger<ProgressGlyphTag>.GetTags(NormalizedSnapshotSpanCollection spans) {
+ if (spans.Count == 0) yield break;
+ var targetSnapshot = spans[0].Snapshot;
+
+ List<SnapshotSpan> pre;
+ List<SnapshotSpan> post;
+ lock (this) {
+ pre = bufferChangesPreVerificationStart;
+ post = bufferChangesPostVerificationStart;
+ }
+
+ // If the requested snapshot isn't the same as the one our words are on, translate our spans to the expected snapshot
+ NormalizedSnapshotSpanCollection chs;
+ chs = new NormalizedSnapshotSpanCollection(Map(pre, span => span.TranslateTo(targetSnapshot, SpanTrackingMode.EdgeExclusive)));
+ foreach (SnapshotSpan span in NormalizedSnapshotSpanCollection.Overlap(spans, chs)) {
+ yield return new TagSpan<ProgressGlyphTag>(span, new ProgressGlyphTag(0));
+ }
+ chs = new NormalizedSnapshotSpanCollection(Map(post, span => span.TranslateTo(targetSnapshot, SpanTrackingMode.EdgeExclusive)));
+ foreach (SnapshotSpan span in NormalizedSnapshotSpanCollection.Overlap(spans, chs)) {
+ yield return new TagSpan<ProgressGlyphTag>(span, new ProgressGlyphTag(1));
+ }
+ }
+
+ /// <summary>
+ /// (Why the firetruck isn't an extension method like this already in the standard library?)
+ /// </summary>
+ public static IEnumerable<TOut> Map<TIn, TOut>(IEnumerable<TIn> coll, System.Func<TIn, TOut> fn) {
+ foreach (var e in coll) {
+ yield return fn(e);
+ }
+ }
+ }
+}
diff --git a/Source/DafnyExtension/Properties/AssemblyInfo.cs b/Source/DafnyExtension/Properties/AssemblyInfo.cs new file mode 100644 index 00000000..b73b8410 --- /dev/null +++ b/Source/DafnyExtension/Properties/AssemblyInfo.cs @@ -0,0 +1,33 @@ +using System.Reflection;
+using System.Runtime.CompilerServices;
+using System.Runtime.InteropServices;
+
+// General Information about an assembly is controlled through the following
+// set of attributes. Change these attribute values to modify the information
+// associated with an assembly.
+[assembly: AssemblyTitle("EditorClassifier1")]
+[assembly: AssemblyDescription("")]
+[assembly: AssemblyConfiguration("")]
+[assembly: AssemblyCompany("")]
+[assembly: AssemblyProduct("EditorClassifier1")]
+[assembly: AssemblyCopyright("")]
+[assembly: AssemblyTrademark("")]
+[assembly: AssemblyCulture("")]
+
+// Setting ComVisible to false makes the types in this assembly not visible
+// to COM components. If you need to access a type in this assembly from
+// COM, set the ComVisible attribute to true on that type.
+[assembly: ComVisible(false)]
+
+// Version information for an assembly consists of the following four values:
+//
+// Major Version
+// Minor Version
+// Build Number
+// Revision
+//
+// You can specify all the values or you can default the Build and Revision Numbers
+// by using the '*' as shown below:
+// [assembly: AssemblyVersion("1.0.*")]
+[assembly: AssemblyVersion("1.0.0.0")]
+[assembly: AssemblyFileVersion("1.0.0.0")]
diff --git a/Source/DafnyExtension/ResolverTagger.cs b/Source/DafnyExtension/ResolverTagger.cs new file mode 100644 index 00000000..d1af6878 --- /dev/null +++ b/Source/DafnyExtension/ResolverTagger.cs @@ -0,0 +1,321 @@ +//***************************************************************************
+// 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;
+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
+{
+ [Export(typeof(ITaggerProvider))]
+ [ContentType("dafny")]
+ [TagType(typeof(DafnyResolverTag))]
+ internal sealed class ResolverTaggerProvider : ITaggerProvider
+ {
+ [Import(typeof(Microsoft.VisualStudio.Shell.SVsServiceProvider))]
+ internal IServiceProvider _serviceProvider = null;
+
+ [Import]
+ ITextDocumentFactoryService _textDocumentFactory = null;
+
+ public ITagger<T> CreateTagger<T>(ITextBuffer buffer) where T : ITag {
+ // create a single tagger for each buffer.
+ Func<ITagger<T>> sc = delegate() { return new ResolverTagger(buffer, _serviceProvider, _textDocumentFactory) as ITagger<T>; };
+ return buffer.Properties.GetOrCreateSingletonProperty<ITagger<T>>(sc);
+ }
+ }
+
+ public abstract class DafnyResolverTag : ITag
+ {
+ }
+ public class DafnyErrorResolverTag : DafnyResolverTag
+ {
+ public readonly string Typ;
+ public readonly string Msg;
+ public DafnyErrorResolverTag(string typ, string msg) {
+ Typ = typ;
+ Msg = msg;
+ }
+ }
+ public class DafnySuccessResolverTag : DafnyResolverTag
+ {
+ public readonly Dafny.Program Program;
+ public DafnySuccessResolverTag(Dafny.Program program) {
+ Program = program;
+ }
+ }
+
+ /// <summary>
+ /// Translate PkgDefTokenTags into ErrorTags and Error List items
+ /// </summary>
+ internal sealed class ResolverTagger : ITagger<DafnyResolverTag>, IDisposable
+ {
+ ITextBuffer _buffer;
+ ITextDocument _document;
+ // 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;
+
+ internal ResolverTagger(ITextBuffer buffer, IServiceProvider serviceProvider, ITextDocumentFactoryService textDocumentFactory) {
+ _buffer = buffer;
+ if (!textDocumentFactory.TryGetTextDocument(_buffer, out _document))
+ _document = null;
+ _snapshot = null; // this makes sure the next snapshot will look different
+ _errorProvider = new ErrorListProvider(serviceProvider);
+
+ BufferIdleEventUtil.AddBufferIdleEventListener(_buffer, ResolveBuffer);
+ }
+
+ public void Dispose() {
+ if (_errorProvider != null) {
+ try {
+ _errorProvider.Tasks.Clear();
+ } catch (InvalidOperationException) {
+ // this may occur if the SVsServiceProvider somehow has been uninstalled before our Dispose method is called
+ }
+ _errorProvider.Dispose();
+ }
+ BufferIdleEventUtil.RemoveBufferIdleEventListener(_buffer, ResolveBuffer);
+ }
+
+ 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()) {
+ 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
+ switch (err.Category) {
+ default: // unexpected category
+ case ErrorCategory.ParseError:
+ case ErrorCategory.ParseWarning:
+ ty = "syntax error"; break; // COLOR: red
+ case ErrorCategory.ResolveError:
+ ty = "compiler error"; break; // COLOR: blue
+ case ErrorCategory.VerificationError:
+ ty = "error"; break; // COLOR: red
+ case ErrorCategory.AuxInformation:
+ ty = "other error"; break; // COLOR: purple red
+ case ErrorCategory.InternalError:
+ ty = "error"; break; // COLOR: red
+ }
+ yield return new TagSpan<DafnyResolverTag>(span, new DafnyErrorResolverTag(ty, err.Message));
+ }
+ }
+
+ ITextSnapshot snap;
+ Dafny.Program prog;
+ lock (this) {
+ snap = _snapshot;
+ prog = _program;
+ }
+ if (prog != null) {
+ yield return new TagSpan<DafnyResolverTag>(new SnapshotSpan(snap, 0, snap.Length), new DafnySuccessResolverTag(prog));
+ }
+ }
+
+ public event EventHandler<SnapshotSpanEventArgs> TagsChanged;
+
+ /// <summary>
+ /// Calls the Dafny parser/resolver/type checker on the contents of the buffer, updates the Error List accordingly.
+ /// </summary>
+ void ResolveBuffer(object sender, EventArgs args) {
+ 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.GetText(), _document != null ? _document.FilePath : "<program>");
+ List<DafnyError> newErrors;
+ Dafny.Program program;
+ try {
+ program = driver.ProcessResolution();
+ newErrors = driver.Errors;
+ } catch (Exception e) {
+ newErrors = new List<DafnyError>();
+ newErrors.Add(new DafnyError(0, 0, ErrorCategory.InternalError, "internal Dafny error: " + e.Message));
+ program = null;
+ }
+
+ lock (this) {
+ _snapshot = snapshot;
+ _program = program;
+ }
+ PopulateErrorList(newErrors, false, snapshot);
+ }
+
+ public void PopulateErrorList(List<DafnyError> newErrors, bool verificationErrors, ITextSnapshot snapshot) {
+ Contract.Requires(newErrors != null);
+ foreach (var err in newErrors) {
+ err.FillInSnapshot(snapshot);
+ }
+ if (verificationErrors) {
+ _verificationErrors = newErrors;
+ } else {
+ _resolutionErrors = newErrors;
+ }
+
+ _errorProvider.SuspendRefresh(); // reduce flickering
+ _errorProvider.Tasks.Clear();
+ foreach (var err in AllErrors()) {
+ ErrorTask task = new ErrorTask() {
+ Category = TaskCategory.BuildCompile,
+ ErrorCategory = CategoryConversion(err.Category),
+ Text = err.Message,
+ Line = err.Line,
+ Column = err.Column
+ };
+ if (_document != null) {
+ task.Document = _document.FilePath;
+ }
+ if (err.Category != ErrorCategory.ProcessError && err.Category != ErrorCategory.InternalError) {
+ task.Navigate += new EventHandler(NavigateHandler);
+ }
+ _errorProvider.Tasks.Add(task);
+ }
+ _errorProvider.ResumeRefresh();
+ var chng = TagsChanged;
+ if (chng != null)
+ chng(this, new SnapshotSpanEventArgs(new SnapshotSpan(snapshot, 0, snapshot.Length)));
+ }
+
+ TaskErrorCategory CategoryConversion(ErrorCategory cat) {
+ switch (cat) {
+ case ErrorCategory.ParseError:
+ case ErrorCategory.ResolveError:
+ case ErrorCategory.VerificationError:
+ case ErrorCategory.InternalError:
+ return TaskErrorCategory.Error;
+ case ErrorCategory.ParseWarning:
+ return TaskErrorCategory.Warning;
+ case ErrorCategory.AuxInformation:
+ return TaskErrorCategory.Message;
+ default:
+ Contract.Assert(false); // unexpected category
+ return TaskErrorCategory.Error; // please compiler
+ }
+ }
+
+ void NavigateHandler(object sender, EventArgs arguments) {
+ var task = sender as ErrorTask;
+ if (task == null || task.Document == null)
+ return;
+
+ // This would have been the simple way of doing things:
+ // _errorProvider.Navigate(error, new Guid(EnvDTE.Constants.vsViewKindCode));
+ // Unfortunately, it doesn't work--it seems to ignore the column position. (Moreover, it wants 1-based
+ // line/column numbers, whereas the Error Task pane wants 0-based line/column numbers.)
+ // So, instead we do all the things that follow:
+
+ var openDoc = Package.GetGlobalService(typeof(IVsUIShellOpenDocument)) as IVsUIShellOpenDocument;
+ if (openDoc == null)
+ return;
+
+ IVsWindowFrame frame;
+ Microsoft.VisualStudio.OLE.Interop.IServiceProvider sp;
+ IVsUIHierarchy hier;
+ uint itemid;
+ Guid logicalView = VSConstants.LOGVIEWID_Code;
+ if (Microsoft.VisualStudio.ErrorHandler.Failed(openDoc.OpenDocumentViaProject(task.Document, ref logicalView, out sp, out hier, out itemid, out frame)) || frame == null)
+ return;
+
+ object docData;
+ Microsoft.VisualStudio.ErrorHandler.ThrowOnFailure(frame.GetProperty((int)__VSFPROPID.VSFPROPID_DocData, out docData));
+
+ // Get the VsTextBuffer
+ VsTextBuffer buffer = docData as VsTextBuffer;
+ if (buffer == null) {
+ IVsTextBufferProvider bufferProvider = docData as IVsTextBufferProvider;
+ if (bufferProvider != null) {
+ IVsTextLines lines;
+ Microsoft.VisualStudio.ErrorHandler.ThrowOnFailure(bufferProvider.GetTextBuffer(out lines));
+ buffer = lines as VsTextBuffer;
+ if (buffer == null)
+ return;
+ }
+ }
+
+ VsTextManager textManager = Package.GetGlobalService(typeof(VsTextManagerClass)) as VsTextManager;
+ if (textManager == null)
+ return;
+
+ // Finally, move the cursor
+ Microsoft.VisualStudio.ErrorHandler.ThrowOnFailure(textManager.NavigateToLineAndColumn(buffer, ref logicalView, task.Line, task.Column, task.Line, task.Column));
+ }
+
+ }
+
+ public enum ErrorCategory
+ {
+ ProcessError, ParseWarning, ParseError, ResolveError, VerificationError, AuxInformation, InternalError
+ }
+
+ internal class DafnyError
+ {
+ public readonly int Line; // 0 based
+ public readonly int Column; // 0 based
+ ITextSnapshot Snapshot; // filled in during the FillInSnapshot call
+ public readonly ErrorCategory Category;
+ public readonly string Message;
+ /// <summary>
+ /// "line" and "col" are expected to be 0-based
+ /// </summary>
+ public DafnyError(int line, int col, ErrorCategory cat, string msg) {
+ Contract.Requires(0 <= line);
+ Contract.Requires(0 <= col);
+ Line = line;
+ Column = col;
+ Category = cat;
+ Message = msg;
+ }
+
+ public void FillInSnapshot(ITextSnapshot snapshot) {
+ Contract.Requires(snapshot != null);
+ Snapshot = snapshot;
+ }
+ public SnapshotSpan Span() {
+ Contract.Requires(Snapshot != null); // requires that Snapshot has been filled in
+ var line = Snapshot.GetLineFromLineNumber(Line);
+ Contract.Assume(Column <= line.Length); // this is really a precondition of the constructor + FillInSnapshot
+ var length = Math.Min(line.Length - Column, 5);
+ return new SnapshotSpan(line.Start + Column, length);
+ }
+ }
+}
diff --git a/Source/DafnyExtension/TokenTagger.cs b/Source/DafnyExtension/TokenTagger.cs new file mode 100644 index 00000000..2f295429 --- /dev/null +++ b/Source/DafnyExtension/TokenTagger.cs @@ -0,0 +1,342 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.ComponentModel.Composition;
+using Microsoft.VisualStudio.Text;
+using Microsoft.VisualStudio.Text.Classification;
+using Microsoft.VisualStudio.Text.Editor;
+using Microsoft.VisualStudio.Text.Tagging;
+using Microsoft.VisualStudio.Utilities;
+using Dafny = Microsoft.Dafny;
+
+namespace DafnyLanguage
+{
+ [Export(typeof(ITaggerProvider))]
+ [ContentType("dafny")]
+ [TagType(typeof(DafnyTokenTag))]
+ internal sealed class DafnyTokenTagProvider : ITaggerProvider
+ {
+ public ITagger<T> CreateTagger<T>(ITextBuffer buffer) where T : ITag {
+ return new DafnyTokenTagger(buffer) as ITagger<T>;
+ }
+ }
+
+ public enum DafnyTokenKinds
+ {
+ Keyword, Number, String, Comment,
+ VariableIdentifier, VariableIdentifierDefinition
+ }
+
+ public class DafnyTokenTag : ITag
+ {
+ public DafnyTokenKinds Kind { get; private set; }
+ public string HoverText { get; private set; }
+
+ public DafnyTokenTag(DafnyTokenKinds kind) {
+ this.Kind = kind;
+ }
+
+ public DafnyTokenTag(DafnyTokenKinds kind, string hoverText) {
+ this.Kind = kind;
+ this.HoverText = hoverText;
+ }
+ }
+
+ internal sealed class DafnyTokenTagger : ITagger<DafnyTokenTag>
+ {
+ ITextBuffer _buffer;
+ ITextSnapshot _snapshot;
+ List<DRegion> _regions;
+
+ internal DafnyTokenTagger(ITextBuffer buffer) {
+ _buffer = buffer;
+ _snapshot = buffer.CurrentSnapshot;
+ _regions = Rescan(_snapshot);
+
+ _buffer.Changed += new EventHandler<TextContentChangedEventArgs>(ReparseFile);
+ }
+
+ public event EventHandler<SnapshotSpanEventArgs> TagsChanged;
+
+ public IEnumerable<ITagSpan<DafnyTokenTag>> GetTags(NormalizedSnapshotSpanCollection spans) {
+ if (spans.Count == 0)
+ yield break;
+
+ List<DRegion> currentRegions = _regions;
+ ITextSnapshot currentSnapshot = _snapshot;
+
+ // create a new SnapshotSpan for the entire region encompassed by the span collection
+ SnapshotSpan entire = new SnapshotSpan(spans[0].Start, spans[spans.Count - 1].End).TranslateTo(currentSnapshot, SpanTrackingMode.EdgeExclusive);
+
+ // return tags for any regions that fall within that span
+ // BUGBUG: depending on how GetTags gets called (e.g., once for each line in the buffer), this may produce quadratic behavior
+ foreach (var region in currentRegions) {
+ if (entire.IntersectsWith(region.Span)) {
+ yield return new TagSpan<DafnyTokenTag>(new SnapshotSpan(region.Start, region.End), new DafnyTokenTag(region.Kind));
+ }
+ }
+ }
+
+ /// <summary>
+ /// Find all of the tag regions in the document (snapshot) and notify
+ /// listeners of any that changed
+ /// </summary>
+ void ReparseFile(object sender, TextContentChangedEventArgs args) {
+ ITextSnapshot snapshot = _buffer.CurrentSnapshot;
+ if (snapshot == _snapshot)
+ return; // we've already computed the regions for this snapshot
+
+ // get all of the outline regions in the snapshot
+ List<DRegion> newRegions = Rescan(snapshot);
+
+ // determine the changed span, and send a changed event with the new spans
+ List<SnapshotSpan> oldSpans = new List<SnapshotSpan>(_regions.Select(r =>
+ r.Span.TranslateTo(snapshot, SpanTrackingMode.EdgeExclusive)));
+
+ List<SnapshotSpan> newSpans = new List<SnapshotSpan>(newRegions.Select(r => r.Span));
+
+ NormalizedSnapshotSpanCollection oldSpanCollection = new NormalizedSnapshotSpanCollection(oldSpans);
+ NormalizedSnapshotSpanCollection newSpanCollection = new NormalizedSnapshotSpanCollection(newSpans);
+
+ NormalizedSnapshotSpanCollection difference = SymmetricDifference(oldSpanCollection, newSpanCollection);
+
+ // save the new baseline
+ _snapshot = snapshot;
+ _regions = newRegions;
+
+ var chng = TagsChanged;
+ if (chng != null) {
+ foreach (var span in difference) {
+ chng(this, new SnapshotSpanEventArgs(span));
+ }
+ }
+ }
+
+ NormalizedSnapshotSpanCollection SymmetricDifference(NormalizedSnapshotSpanCollection first, NormalizedSnapshotSpanCollection second) {
+ return NormalizedSnapshotSpanCollection.Union(
+ NormalizedSnapshotSpanCollection.Difference(first, second),
+ NormalizedSnapshotSpanCollection.Difference(second, first));
+ }
+
+ private static List<DRegion> Rescan(ITextSnapshot newSnapshot) {
+ List<DRegion> newRegions = new List<DRegion>();
+
+ bool stillScanningLongComment = false;
+ SnapshotPoint commentStart = new SnapshotPoint(); // used only when stillScanningLongComment
+ SnapshotPoint commentEndAsWeKnowIt = new SnapshotPoint(); // used only when stillScanningLongComment
+ foreach (ITextSnapshotLine line in newSnapshot.Lines) {
+ string txt = line.GetText(); // the current line (without linebreak characters)
+ int N = txt.Length; // length of the current line
+ int cur = 0; // offset into the current line
+
+ if (stillScanningLongComment) {
+ if (ScanForEndOfComment(txt, ref cur)) {
+ newRegions.Add(new DRegion(commentStart, new SnapshotPoint(newSnapshot, line.Start + cur), DafnyTokenKinds.Comment));
+ stillScanningLongComment = false;
+ } else {
+ commentEndAsWeKnowIt = new SnapshotPoint(newSnapshot, line.Start + cur);
+ }
+ }
+
+ // repeatedly get the remaining tokens from this line
+ int end; // offset into the current line
+ for (; ; cur = end) {
+ // advance to the first character of a keyword or token
+ DafnyTokenKinds ty = DafnyTokenKinds.Keyword;
+ for (; ; cur++) {
+ if (N <= cur) {
+ // we've looked at everything in this line
+ goto OUTER_CONTINUE;
+ }
+ char ch = txt[cur];
+ if ('a' <= ch && ch <= 'z') break;
+ if ('A' <= ch && ch <= 'Z') break;
+ if ('0' <= ch && ch <= '9') { ty = DafnyTokenKinds.Number; break; }
+ if (ch == '"') { ty = DafnyTokenKinds.String; break; }
+ if (ch == '/') { ty = DafnyTokenKinds.Comment; break; }
+ if (ch == '\'' || ch == '_' || ch == '?' || ch == '\\') break; // parts of identifiers
+ }
+
+ // advance to the end of the token
+ end = cur + 1; // offset into the current line
+ if (ty == DafnyTokenKinds.Number) {
+ // scan the rest of this number
+ for (; end < N; end++) {
+ char ch = txt[end];
+ if ('0' <= ch && ch <= '9') {
+ } else break;
+ }
+ } else if (ty == DafnyTokenKinds.String) {
+ // scan the rest of this string, but not past the end-of-line
+ for (; end < N; end++) {
+ char ch = txt[end];
+ if (ch == '"') {
+ end++; break;
+ } else if (ch == '\\') {
+ // escape sequence
+ end++;
+ if (end == N) { break; }
+ ch = txt[end];
+ if (ch == 'u') {
+ end += 4;
+ if (N <= end) { end = N; break; }
+ }
+ }
+ }
+ } else if (ty == DafnyTokenKinds.Comment) {
+ if (end == N) continue; // this was not the start of a comment
+ char ch = txt[end];
+ if (ch == '/') {
+ // a short comment
+ end = N;
+ } else if (ch == '*') {
+ // a long comment; find the matching "*/"
+ end++;
+ commentStart = new SnapshotPoint(newSnapshot, line.Start + cur);
+ if (ScanForEndOfComment(txt, ref end)) {
+ newRegions.Add(new DRegion(commentStart, new SnapshotPoint(newSnapshot, line.Start + end), DafnyTokenKinds.Comment));
+ } else {
+ stillScanningLongComment = true;
+ commentEndAsWeKnowIt = new SnapshotPoint(newSnapshot, line.Start + end);
+ }
+ continue;
+ } else {
+ // not a comment
+ continue;
+ }
+ } else {
+ int trailingDigits = 0;
+ for (; end < N; end++) {
+ char ch = txt[end];
+ if ('a' <= ch && ch <= 'z') {
+ trailingDigits = 0;
+ } else if ('A' <= ch && ch <= 'Z') {
+ trailingDigits = 0;
+ } else if ('0' <= ch && ch <= '9') {
+ trailingDigits++;
+ } else if (ch == '\'' || ch == '_' || ch == '?' || ch == '\\') {
+ trailingDigits = 0;
+ } else break;
+ }
+ // we have a keyword or an identifier
+ string s = txt.Substring(cur, end - cur);
+ if (0 < trailingDigits && s.Length == 5 + trailingDigits && s.StartsWith("array") && s[5] != '0' && (trailingDigits != 1 || s[5] != '1')) {
+ // this is a keyword (array2, array3, ...)
+ } else {
+ switch (s) {
+ #region keywords
+ case "allocated":
+ case "array":
+ case "as":
+ case "assert":
+ case "assume":
+ case "bool":
+ case "break":
+ case "calc":
+ case "case":
+ case "choose":
+ case "class":
+ case "codatatype":
+ case "constructor":
+ case "copredicate":
+ case "datatype":
+ case "decreases":
+ case "else":
+ case "ensures":
+ case "exists":
+ case "false":
+ case "forall":
+ case "free":
+ case "fresh":
+ case "function":
+ case "ghost":
+ case "if":
+ case "import":
+ case "in":
+ case "int":
+ case "invariant":
+ case "iterator":
+ case "label":
+ case "match":
+ case "method":
+ case "modifies":
+ case "module":
+ case "multiset":
+ case "nat":
+ case "new":
+ case "null":
+ case "object":
+ case "old":
+ case "opened":
+ case "parallel":
+ case "predicate":
+ case "print":
+ case "reads":
+ case "refines":
+ case "requires":
+ case "result":
+ case "return":
+ case "returns":
+ case "seq":
+ case "set":
+ case "static":
+ case "then":
+ case "this":
+ case "true":
+ case "type":
+ case "var":
+ case "while":
+ case "yield":
+ case "yields":
+ #endregion
+ break;
+ default:
+ continue; // it was an identifier
+ }
+ }
+ }
+
+ newRegions.Add(new DRegion(new SnapshotPoint(newSnapshot, line.Start + cur), new SnapshotPoint(newSnapshot, line.Start + end), ty));
+ }
+ OUTER_CONTINUE: ;
+ }
+
+ if (stillScanningLongComment) {
+ newRegions.Add(new DRegion(commentStart, commentEndAsWeKnowIt, DafnyTokenKinds.Comment));
+ }
+
+ return newRegions;
+ }
+
+ private static bool ScanForEndOfComment(string txt, ref int end) {
+ int N = txt.Length;
+ for (; end < N; end++) {
+ char ch = txt[end];
+ if (ch == '*' && end + 1 < N) {
+ ch = txt[end + 1];
+ if (ch == '/') {
+ end += 2;
+ return true;
+ }
+ }
+ }
+ return false; // hit end-of-line without finding end-of-comment
+ }
+ }
+
+ internal class DRegion
+ {
+ public SnapshotPoint Start { get; private set; }
+ public SnapshotPoint End { get; private set; }
+ public SnapshotSpan Span {
+ get { return new SnapshotSpan(Start, End); }
+ }
+ public DafnyTokenKinds Kind { get; private set; }
+
+ public DRegion(SnapshotPoint start, SnapshotPoint end, DafnyTokenKinds kind) {
+ Start = start;
+ End = end;
+ Kind = kind;
+ }
+ }
+}
diff --git a/Source/DafnyExtension/WordHighlighter.cs b/Source/DafnyExtension/WordHighlighter.cs new file mode 100644 index 00000000..03456c85 --- /dev/null +++ b/Source/DafnyExtension/WordHighlighter.cs @@ -0,0 +1,211 @@ +using System;
+using System.Collections.Generic;
+using System.ComponentModel.Composition;
+using System.Linq;
+using System.Threading;
+using System.Windows.Media;
+using Microsoft.VisualStudio.Text;
+using Microsoft.VisualStudio.Text.Classification;
+using Microsoft.VisualStudio.Text.Editor;
+using Microsoft.VisualStudio.Text.Operations;
+using Microsoft.VisualStudio.Text.Tagging;
+using Microsoft.VisualStudio.Utilities;
+
+namespace DafnyLanguage
+{
+#if LATER_MAYBE
+ #region // (the current annoying) word highligher
+ internal class HighlightWordTagger : ITagger<HighlightWordTag>
+ {
+ ITextView View { get; set; }
+ ITextBuffer SourceBuffer { get; set; }
+ ITextSearchService TextSearchService { get; set; }
+ ITextStructureNavigator TextStructureNavigator { get; set; }
+ NormalizedSnapshotSpanCollection WordSpans { get; set; }
+ SnapshotSpan? CurrentWord { get; set; }
+ SnapshotPoint RequestedPoint { get; set; }
+ object updateLock = new object();
+
+ public HighlightWordTagger(ITextView view, ITextBuffer sourceBuffer, ITextSearchService textSearchService,
+ ITextStructureNavigator textStructureNavigator) {
+ this.View = view;
+ this.SourceBuffer = sourceBuffer;
+ this.TextSearchService = textSearchService;
+ this.TextStructureNavigator = textStructureNavigator;
+ this.WordSpans = new NormalizedSnapshotSpanCollection();
+ this.CurrentWord = null;
+ this.View.Caret.PositionChanged += CaretPositionChanged;
+ this.View.LayoutChanged += ViewLayoutChanged;
+ }
+
+ void ViewLayoutChanged(object sender, TextViewLayoutChangedEventArgs e) {
+ // If a new snapshot wasn't generated, then skip this layout
+ if (e.NewSnapshot != e.OldSnapshot) {
+ UpdateAtCaretPosition(View.Caret.Position);
+ }
+ }
+
+ void CaretPositionChanged(object sender, CaretPositionChangedEventArgs e) {
+ UpdateAtCaretPosition(e.NewPosition);
+ }
+
+ public event EventHandler<SnapshotSpanEventArgs> TagsChanged;
+
+ void UpdateAtCaretPosition(CaretPosition caretPosition) {
+ SnapshotPoint? point = caretPosition.Point.GetPoint(SourceBuffer, caretPosition.Affinity);
+
+ if (!point.HasValue)
+ return;
+
+ // If the new caret position is still within the current word (and on the same snapshot), we don't need to check it
+ if (CurrentWord.HasValue
+ && CurrentWord.Value.Snapshot == View.TextSnapshot
+ && CurrentWord.Value.Start <= point.Value && point.Value <= CurrentWord.Value.End) {
+ return;
+ }
+
+ RequestedPoint = point.Value;
+ UpdateWordAdornments();
+ }
+
+ void UpdateWordAdornments() {
+ SnapshotPoint currentRequest = RequestedPoint;
+ List<SnapshotSpan> wordSpans = new List<SnapshotSpan>();
+ //Find all words in the buffer like the one the caret is on
+ TextExtent word = TextStructureNavigator.GetExtentOfWord(currentRequest);
+ bool foundWord = true;
+ //If we've selected something not worth highlighting, we might have missed a "word" by a little bit
+ if (!WordExtentIsValid(currentRequest, word)) {
+ //Before we retry, make sure it is worthwhile
+ if (word.Span.Start != currentRequest
+ || currentRequest == currentRequest.GetContainingLine().Start
+ || char.IsWhiteSpace((currentRequest - 1).GetChar())) {
+ foundWord = false;
+ } else {
+ // Try again, one character previous.
+ //If the caret is at the end of a word, pick up the word.
+ word = TextStructureNavigator.GetExtentOfWord(currentRequest - 1);
+
+ //If the word still isn't valid, we're done
+ if (!WordExtentIsValid(currentRequest, word))
+ foundWord = false;
+ }
+ }
+
+ if (!foundWord) {
+ //If we couldn't find a word, clear out the existing markers
+ SynchronousUpdate(currentRequest, new NormalizedSnapshotSpanCollection(), null);
+ return;
+ }
+
+ SnapshotSpan currentWord = word.Span;
+ //If this is the current word, and the caret moved within a word, we're done.
+ if (CurrentWord.HasValue && currentWord == CurrentWord)
+ return;
+
+ //Find the new spans
+ FindData findData = new FindData(currentWord.GetText(), currentWord.Snapshot);
+ findData.FindOptions = FindOptions.WholeWord | FindOptions.MatchCase;
+
+ wordSpans.AddRange(TextSearchService.FindAll(findData));
+
+ //If another change hasn't happened, do a real update
+ if (currentRequest == RequestedPoint)
+ SynchronousUpdate(currentRequest, new NormalizedSnapshotSpanCollection(wordSpans), currentWord);
+ }
+
+ static bool WordExtentIsValid(SnapshotPoint currentRequest, TextExtent word) {
+ return word.IsSignificant
+ && currentRequest.Snapshot.GetText(word.Span).Any(c => char.IsLetter(c));
+ }
+
+ void SynchronousUpdate(SnapshotPoint currentRequest, NormalizedSnapshotSpanCollection newSpans, SnapshotSpan? newCurrentWord) {
+ lock (updateLock) {
+ if (currentRequest != RequestedPoint)
+ return;
+
+ WordSpans = newSpans;
+ CurrentWord = newCurrentWord;
+
+ var chngd = TagsChanged;
+ if (chngd != null)
+ chngd(this, new SnapshotSpanEventArgs(new SnapshotSpan(SourceBuffer.CurrentSnapshot, 0, SourceBuffer.CurrentSnapshot.Length)));
+ }
+ }
+
+ public IEnumerable<ITagSpan<HighlightWordTag>> GetTags(NormalizedSnapshotSpanCollection spans) {
+ if (CurrentWord == null)
+ yield break;
+
+ // Hold on to a "snapshot" of the word spans and current word, so that we maintain the same
+ // collection throughout
+ SnapshotSpan currentWord = CurrentWord.Value;
+ NormalizedSnapshotSpanCollection wordSpans = WordSpans;
+
+ if (spans.Count == 0 || WordSpans.Count == 0)
+ yield break;
+
+ // If the requested snapshot isn't the same as the one our words are on, translate our spans to the expected snapshot
+ if (spans[0].Snapshot != wordSpans[0].Snapshot) {
+ wordSpans = new NormalizedSnapshotSpanCollection(
+ wordSpans.Select(span => span.TranslateTo(spans[0].Snapshot, SpanTrackingMode.EdgeExclusive)));
+
+ currentWord = currentWord.TranslateTo(spans[0].Snapshot, SpanTrackingMode.EdgeExclusive);
+ }
+
+ // First, yield back the word the cursor is under (if it overlaps)
+ // Note that we'll yield back the same word again in the wordspans collection;
+ // the duplication here is expected.
+ if (spans.OverlapsWith(new NormalizedSnapshotSpanCollection(currentWord)))
+ yield return new TagSpan<HighlightWordTag>(currentWord, new HighlightWordTag());
+
+ // Second, yield all the other words in the file
+ foreach (SnapshotSpan span in NormalizedSnapshotSpanCollection.Overlap(spans, wordSpans)) {
+ yield return new TagSpan<HighlightWordTag>(span, new HighlightWordTag());
+ }
+ }
+ }
+
+ internal class HighlightWordTag : TextMarkerTag
+ {
+ public HighlightWordTag() : base("MarkerFormatDefinition/HighlightWordFormatDefinition") { }
+ }
+
+ [Export(typeof(EditorFormatDefinition))]
+ [Name("MarkerFormatDefinition/HighlightWordFormatDefinition")]
+ [UserVisible(true)]
+ internal class HighlightWordFormatDefinition : MarkerFormatDefinition
+ {
+ public HighlightWordFormatDefinition() {
+ this.BackgroundColor = Colors.LightBlue;
+ this.ForegroundColor = Colors.DarkBlue;
+ this.DisplayName = "Highlight Word";
+ this.ZOrder = 5;
+ }
+ }
+
+ [Export(typeof(IViewTaggerProvider))]
+ [ContentType("text")]
+ [TagType(typeof(TextMarkerTag))]
+ internal class HighlightWordTaggerProvider : IViewTaggerProvider
+ {
+ [Import]
+ internal ITextSearchService TextSearchService { get; set; }
+
+ [Import]
+ internal ITextStructureNavigatorSelectorService TextStructureNavigatorSelector { get; set; }
+
+ public ITagger<T> CreateTagger<T>(ITextView textView, ITextBuffer buffer) where T : ITag {
+ //provide highlighting only on the top buffer
+ if (textView.TextBuffer != buffer)
+ return null;
+
+ ITextStructureNavigator textStructureNavigator =
+ TextStructureNavigatorSelector.GetTextStructureNavigator(buffer);
+
+ return new HighlightWordTagger(textView, buffer, TextSearchService, textStructureNavigator) as ITagger<T>;
+ }
+ }
+#endregion
+#endif
+}
diff --git a/Source/DafnyExtension/source.extension.vsixmanifest b/Source/DafnyExtension/source.extension.vsixmanifest new file mode 100644 index 00000000..ef5c1cf5 --- /dev/null +++ b/Source/DafnyExtension/source.extension.vsixmanifest @@ -0,0 +1,25 @@ +<?xml version="1.0" encoding="utf-8"?>
+<Vsix xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns:xsd="http://www.w3.org/2001/XMLSchema" Version="1.0.0" xmlns="http://schemas.microsoft.com/developer/vsx-schema/2010">
+ <Identifier Id="DafnyLanguageMode.Microsoft.6c7ed99a-206a-4937-9e08-b389de175f68">
+ <Name>DafnyLanguageMode</Name>
+ <Author>Microsoft Research</Author>
+ <Version>1.0</Version>
+ <Description xml:space="preserve">This is a language mode for using the Dafny language inside Visual Studio.</Description>
+ <Locale>1033</Locale>
+ <SupportedProducts>
+ <VisualStudio Version="10.0">
+ <Edition>Pro</Edition>
+ </VisualStudio>
+ <VisualStudio Version="11.0">
+ <Edition>Pro</Edition>
+ </VisualStudio>
+ </SupportedProducts>
+ <SupportedFrameworkRuntimeEdition MinVersion="4.0" MaxVersion="4.0" />
+ </Identifier>
+ <References />
+ <Content>
+ <MefComponent>|%CurrentProject%|</MefComponent>
+ <CustomExtension Type="Boogie">DafnyPrelude.bpl</CustomExtension>
+ <CustomExtension Type="SMTLib 2">UnivBackPred2.smt2</CustomExtension>
+ </Content>
+</Vsix>
|