From 8911e5c95d4715c2e2626aef67f19793d6f43201 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Thu, 4 Oct 2012 13:32:50 -0700 Subject: Put all sources under \Source directory --- Util/VS2010/DafnyExtension/DafnyExtension.sln | 20 - .../DafnyExtension/DafnyExtension/BraceMatching.cs | 253 ------------- .../DafnyExtension/BufferIdleEventUtil.cs | 155 -------- .../DafnyExtension/ClassificationTagger.cs | 107 ------ .../DafnyExtension/DafnyExtension/ContentType.cs | 18 - .../DafnyExtension/DafnyExtension/DafnyDriver.cs | 419 --------------------- .../DafnyExtension/DafnyExtension.csproj | 191 ---------- .../DafnyExtension/DafnyExtension/ErrorTagger.cs | 85 ----- .../DafnyExtension/DafnyExtension/HoverText.cs | 126 ------- .../DafnyExtension/IdentifierTagger.cs | 344 ----------------- .../DafnyExtension/OutliningTagger.cs | 185 --------- .../DafnyExtension/ProgressMargin.cs | 260 ------------- .../DafnyExtension/Properties/AssemblyInfo.cs | 33 -- .../DafnyExtension/ResolverTagger.cs | 321 ---------------- .../DafnyExtension/DafnyExtension/TokenTagger.cs | 342 ----------------- .../DafnyExtension/WordHighlighter.cs | 211 ----------- .../DafnyExtension/source.extension.vsixmanifest | 25 -- 17 files changed, 3095 deletions(-) delete mode 100644 Util/VS2010/DafnyExtension/DafnyExtension.sln delete mode 100644 Util/VS2010/DafnyExtension/DafnyExtension/BraceMatching.cs delete mode 100644 Util/VS2010/DafnyExtension/DafnyExtension/BufferIdleEventUtil.cs delete mode 100644 Util/VS2010/DafnyExtension/DafnyExtension/ClassificationTagger.cs delete mode 100644 Util/VS2010/DafnyExtension/DafnyExtension/ContentType.cs delete mode 100644 Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs delete mode 100644 Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj delete mode 100644 Util/VS2010/DafnyExtension/DafnyExtension/ErrorTagger.cs delete mode 100644 Util/VS2010/DafnyExtension/DafnyExtension/HoverText.cs delete mode 100644 Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs delete mode 100644 Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs delete mode 100644 Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs delete mode 100644 Util/VS2010/DafnyExtension/DafnyExtension/Properties/AssemblyInfo.cs delete mode 100644 Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs delete mode 100644 Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs delete mode 100644 Util/VS2010/DafnyExtension/DafnyExtension/WordHighlighter.cs delete mode 100644 Util/VS2010/DafnyExtension/DafnyExtension/source.extension.vsixmanifest (limited to 'Util') diff --git a/Util/VS2010/DafnyExtension/DafnyExtension.sln b/Util/VS2010/DafnyExtension/DafnyExtension.sln deleted file mode 100644 index fd450cc8..00000000 --- a/Util/VS2010/DafnyExtension/DafnyExtension.sln +++ /dev/null @@ -1,20 +0,0 @@ - -Microsoft Visual Studio Solution File, Format Version 12.00 -# Visual Studio 2012 -Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyExtension", "DafnyExtension\DafnyExtension.csproj", "{6E9A5E14-0763-471C-A129-80A879D9E7BA}" -EndProject -Global - GlobalSection(SolutionConfigurationPlatforms) = preSolution - Debug|Any CPU = Debug|Any CPU - Release|Any CPU = Release|Any CPU - EndGlobalSection - GlobalSection(ProjectConfigurationPlatforms) = postSolution - {6E9A5E14-0763-471C-A129-80A879D9E7BA}.Debug|Any CPU.ActiveCfg = Debug|Any CPU - {6E9A5E14-0763-471C-A129-80A879D9E7BA}.Debug|Any CPU.Build.0 = Debug|Any CPU - {6E9A5E14-0763-471C-A129-80A879D9E7BA}.Release|Any CPU.ActiveCfg = Release|Any CPU - {6E9A5E14-0763-471C-A129-80A879D9E7BA}.Release|Any CPU.Build.0 = Release|Any CPU - EndGlobalSection - GlobalSection(SolutionProperties) = preSolution - HideSolutionNode = FALSE - EndGlobalSection -EndGlobal diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/BraceMatching.cs b/Util/VS2010/DafnyExtension/DafnyExtension/BraceMatching.cs deleted file mode 100644 index 44b1affe..00000000 --- a/Util/VS2010/DafnyExtension/DafnyExtension/BraceMatching.cs +++ /dev/null @@ -1,253 +0,0 @@ -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 CreateTagger(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 tagAggregator = AggregatorFactory.CreateTagAggregator(buffer); - return new BraceMatchingTagger(textView, buffer, tagAggregator) as ITagger; - } - } - - internal abstract class TokenBasedTagger - { - ITagAggregator _aggregator; - - internal TokenBasedTagger(ITagAggregator 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 - { - 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 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 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> 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(new SnapshotSpan(currentChar, 1), Blue); - yield return new TagSpan(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(new SnapshotSpan(prevChar, 1), Blue); - yield return new TagSpan(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/Util/VS2010/DafnyExtension/DafnyExtension/BufferIdleEventUtil.cs b/Util/VS2010/DafnyExtension/DafnyExtension/BufferIdleEventUtil.cs deleted file mode 100644 index 1aea1385..00000000 --- a/Util/VS2010/DafnyExtension/DafnyExtension/BufferIdleEventUtil.cs +++ /dev/null @@ -1,155 +0,0 @@ -//*************************************************************************** -// 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 -{ - /// - /// 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 - /// - 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 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 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 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 ConnectToBuffer(ITextBuffer buffer) - { - buffer.Changed += BufferChanged; - - RestartTimerForBuffer(buffer); - - HashSet listenersForBuffer = new HashSet(); - 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 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/Util/VS2010/DafnyExtension/DafnyExtension/ClassificationTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/ClassificationTagger.cs deleted file mode 100644 index 09835ac9..00000000 --- a/Util/VS2010/DafnyExtension/DafnyExtension/ClassificationTagger.cs +++ /dev/null @@ -1,107 +0,0 @@ -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 CreateTagger(ITextBuffer buffer) where T : ITag { - ITagAggregator tagAggregator = AggregatorFactory.CreateTagAggregator(buffer); - return new DafnyClassifier(buffer, tagAggregator, ClassificationTypeRegistry, Standards) as ITagger; - } - } - - internal sealed class DafnyClassifier : ITagger - { - ITextBuffer _buffer; - ITagAggregator _aggregator; - IDictionary _typeMap; - - internal DafnyClassifier(ITextBuffer buffer, - ITagAggregator tagAggregator, - IClassificationTypeRegistryService typeService, Microsoft.VisualStudio.Language.StandardClassification.IStandardClassificationService standards) { - _buffer = buffer; - _aggregator = tagAggregator; - _aggregator.TagsChanged += new EventHandler(_aggregator_TagsChanged); - // use built-in classification types: - _typeMap = new Dictionary(); - _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 TagsChanged; - - public IEnumerable> 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(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)); - } - } - } - } - - /// - /// Defines an editor format for user-defined type. - /// - [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 - { - /// - /// Defines the "ordinary" classification type. - /// - [Export(typeof(ClassificationTypeDefinition))] - [Name("Dafny identifier")] - internal static ClassificationTypeDefinition UserType = null; - } -} diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/ContentType.cs b/Util/VS2010/DafnyExtension/DafnyExtension/ContentType.cs deleted file mode 100644 index d8487f74..00000000 --- a/Util/VS2010/DafnyExtension/DafnyExtension/ContentType.cs +++ /dev/null @@ -1,18 +0,0 @@ -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/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs deleted file mode 100644 index 39829bb0..00000000 --- a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyDriver.cs +++ /dev/null @@ -1,419 +0,0 @@ -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 _errors = new List(); - public List 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 } - - /// - /// 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. - /// - 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; - } - } - } - } - } - - /// - /// 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 - /// - 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; - } - - /// - /// 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 - /// - 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/*?*/ 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 Aux = new List(); - - 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/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj deleted file mode 100644 index 2580c396..00000000 --- a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj +++ /dev/null @@ -1,191 +0,0 @@ - - - - - Debug - AnyCPU - 10.0.20305 - 2.0 - {82b43b9b-a64c-4715-b499-d71e9ca2bd60};{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC} - {6E9A5E14-0763-471C-A129-80A879D9E7BA} - Library - Properties - DafnyLanguage - DafnyLanguageService - v4.0 - 512 - false - 11.0 - - - - - 4.0 - - - true - full - false - bin\Debug\ - DEBUG;TRACE - prompt - 4 - - - pdbonly - true - bin\Release\ - TRACE - prompt - 4 - - - - False - ..\..\..\..\Binaries\AbsInt.dll - - - False - ..\..\..\..\Binaries\AIFramework.dll - - - False - ..\..\..\..\Binaries\Basetypes.dll - - - False - ..\..\..\..\Binaries\CodeContractsExtender.dll - - - False - ..\..\..\..\Binaries\Core.dll - - - False - ..\..\..\..\Binaries\DafnyPipeline.dll - - - ..\..\..\..\Binaries\Graph.dll - - - ..\..\..\..\Binaries\Houdini.dll - - - ..\..\..\..\Binaries\Model.dll - - - ..\..\..\..\Binaries\ParserHelper.dll - - - ..\..\..\..\Binaries\Provers.Z3.dll - - - ..\..\..\..\Binaries\Provers.SMTLib.dll - - - ..\..\..\..\Binaries\VCExpr.dll - - - False - ..\..\..\..\Binaries\VCGeneration.dll - - - False - - - False - - - - - - - False - - - - - True - - - - False - - - False - - - False - - - False - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - true - Always - - - Designer - - - true - Always - - - - - - - 10.0 - $(MSBuildExtensionsPath32)\Microsoft\VisualStudio\v$(VisualStudioVersion) - - - - - - cd - - - - - copy ..\..\..\..\..\..\Binaries\DafnyPrelude.bpl $(ProjectDir) -copy ..\..\..\..\..\..\Binaries\UnivBackPred2.smt2 $(ProjectDir) - - - \ No newline at end of file diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/ErrorTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/ErrorTagger.cs deleted file mode 100644 index efd755d8..00000000 --- a/Util/VS2010/DafnyExtension/DafnyExtension/ErrorTagger.cs +++ /dev/null @@ -1,85 +0,0 @@ -//*************************************************************************** -// 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 CreateTagger(ITextBuffer buffer) where T : ITag { - ITagAggregator tagAggregator = AggregatorFactory.CreateTagAggregator(buffer); - // create a single tagger for each buffer. - Func> sc = delegate() { return new ErrorTagger(buffer, tagAggregator) as ITagger; }; - return buffer.Properties.GetOrCreateSingletonProperty>(sc); - } - } - - /// - /// Translate PkgDefTokenTags into ErrorTags and Error List items - /// - internal sealed class ErrorTagger : ITagger - { - ITextBuffer _buffer; - ITagAggregator _aggregator; - - internal ErrorTagger(ITextBuffer buffer, ITagAggregator tagAggregator) { - _buffer = buffer; - _aggregator = tagAggregator; - _aggregator.TagsChanged += new EventHandler(_aggregator_TagsChanged); - } - - /// - /// Find the Error tokens in the set of all tokens and create an ErrorTag for each - /// - public IEnumerable> GetTags(NormalizedSnapshotSpanCollection spans) { - if (spans.Count == 0) yield break; - 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(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 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/Util/VS2010/DafnyExtension/DafnyExtension/HoverText.cs b/Util/VS2010/DafnyExtension/DafnyExtension/HoverText.cs deleted file mode 100644 index be806f5b..00000000 --- a/Util/VS2010/DafnyExtension/DafnyExtension/HoverText.cs +++ /dev/null @@ -1,126 +0,0 @@ -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(textBuffer)); - } - } - - class DafnyQuickInfoSource : IQuickInfoSource - { - private ITagAggregator _aggregator; - private ITextBuffer _buffer; - - public DafnyQuickInfoSource(ITextBuffer buffer, ITagAggregator aggregator) { - _aggregator = aggregator; - _buffer = buffer; - } - - public void AugmentQuickInfoSession(IQuickInfoSession session, IList quickInfoContent, out ITrackingSpan applicableToSpan) { - applicableToSpan = null; - - var triggerPoint = (SnapshotPoint)session.GetTriggerPoint(_buffer.CurrentSnapshot); - if (triggerPoint == null) - return; - - foreach (IMappingTagSpan curTag in _aggregator.GetTags(new SnapshotSpan(triggerPoint, triggerPoint))) { - var s = curTag.Tag.HoverText; - if (s != null) { - var tagSpan = curTag.Span.GetSpans(_buffer).First(); - applicableToSpan = _buffer.CurrentSnapshot.CreateTrackingSpan(tagSpan, SpanTrackingMode.EdgeExclusive); - quickInfoContent.Add(s); - } - } - } - public void Dispose() { - } - } - // --------------------------------- QuickInfo controller ------------------------------------------ - - [Export(typeof(IIntellisenseControllerProvider))] - [Name("Dafny QuickInfo controller")] - [ContentType("dafny")] - class DafnyQuickInfoControllerProvider : IIntellisenseControllerProvider - { - [Import] - internal IQuickInfoBroker QuickInfoBroker { get; set; } - - public IIntellisenseController TryCreateIntellisenseController(ITextView textView, IList subjectBuffers) { - return new DafnyQuickInfoController(textView, subjectBuffers, this); - } - } - - class DafnyQuickInfoController : IIntellisenseController - { - private ITextView _textView; - private IList _subjectBuffers; - private DafnyQuickInfoControllerProvider _componentContext; - - private IQuickInfoSession _session; - - internal DafnyQuickInfoController(ITextView textView, IList subjectBuffers, DafnyQuickInfoControllerProvider componentContext) { - _textView = textView; - _subjectBuffers = subjectBuffers; - _componentContext = componentContext; - - _textView.MouseHover += this.OnTextViewMouseHover; - } - - public void ConnectSubjectBuffer(ITextBuffer subjectBuffer) { - } - - public void DisconnectSubjectBuffer(ITextBuffer subjectBuffer) { - } - - public void Detach(ITextView textView) { - if (_textView == textView) { - _textView.MouseHover -= OnTextViewMouseHover; - _textView = null; - } - } - - void OnTextViewMouseHover(object sender, MouseHoverEventArgs e) { - SnapshotPoint? point = GetMousePosition(new SnapshotPoint(_textView.TextSnapshot, e.Position)); - - if (point != null) { - ITrackingPoint triggerPoint = point.Value.Snapshot.CreateTrackingPoint(point.Value.Position, PointTrackingMode.Positive); - - // Find the broker for this buffer - if (!_componentContext.QuickInfoBroker.IsQuickInfoActive(_textView)) { - _session = _componentContext.QuickInfoBroker.CreateQuickInfoSession(_textView, triggerPoint, true); - _session.Start(); - } - } - } - - SnapshotPoint? GetMousePosition(SnapshotPoint topPosition) { - return _textView.BufferGraph.MapDownToFirstMatch( - topPosition, - PointTrackingMode.Positive, - snapshot => _subjectBuffers.Contains(snapshot.TextBuffer), - PositionAffinity.Predecessor); - } - } -} diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs deleted file mode 100644 index 5ecc8dc2..00000000 --- a/Util/VS2010/DafnyExtension/DafnyExtension/IdentifierTagger.cs +++ /dev/null @@ -1,344 +0,0 @@ -//*************************************************************************** -// 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 CreateTagger(ITextBuffer buffer) where T : ITag { - ITagAggregator tagAggregator = AggregatorFactory.CreateTagAggregator(buffer); - // create a single tagger for each buffer. - Func> sc = delegate() { return new IdentifierTagger(buffer, tagAggregator) as ITagger; }; - return buffer.Properties.GetOrCreateSingletonProperty>(sc); - } - } - - /// - /// Translate DafnyResolverTag's into IOutliningRegionTag's - /// - internal sealed class IdentifierTagger : ITagger - { - ITextBuffer _buffer; - ITextSnapshot _snapshot; // the most recent snapshot of _buffer that we have been informed about - Microsoft.Dafny.Program _program; // the program parsed from _snapshot - List _regions = new List(); // the regions generated from _program - ITagAggregator _aggregator; - - internal IdentifierTagger(ITextBuffer buffer, ITagAggregator tagAggregator) { - _buffer = buffer; - _snapshot = _buffer.CurrentSnapshot; - _aggregator = tagAggregator; - _aggregator.TagsChanged += new EventHandler(_aggregator_TagsChanged); - } - - /// - /// Find the Error tokens in the set of all tokens and create an ErrorTag for each - /// - public IEnumerable> GetTags(NormalizedSnapshotSpanCollection spans) { - if (spans.Count == 0) yield break; - // (A NormalizedSnapshotSpanCollection contains spans that all come from the same snapshot.) - // The spans are ordered by the .Start component, and the collection contains no adjacent or abutting spans. - // Hence, to find a span that includes all the ones in "spans", we only need to look at the .Start for the - // first spand and the .End of the last span: - var startPoint = spans[0].Start; - var endPoint = spans[spans.Count - 1].End; - - // Note, (startPoint,endPoint) are points in the spans for which we're being asked to provide tags. We need to translate - // these back into the most recent snapshot that we've computed regions for, namely _snapshot. - var entire = new SnapshotSpan(startPoint, endPoint).TranslateTo(_snapshot, SpanTrackingMode.EdgeExclusive); - int start = entire.Start; - int end = entire.End; - foreach (var r in _regions) { - if (0 <= r.Length && r.Start <= end && start <= r.Start + r.Length) { - 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( - 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 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 newRegions = new List(); - - 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 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 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 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 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 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/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs deleted file mode 100644 index a47cdba7..00000000 --- a/Util/VS2010/DafnyExtension/DafnyExtension/OutliningTagger.cs +++ /dev/null @@ -1,185 +0,0 @@ -//*************************************************************************** -// 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 CreateTagger(ITextBuffer buffer) where T : ITag { - ITagAggregator tagAggregator = AggregatorFactory.CreateTagAggregator(buffer); - // create a single tagger for each buffer. - Func> sc = delegate() { return new OutliningTagger(buffer, tagAggregator) as ITagger; }; - return buffer.Properties.GetOrCreateSingletonProperty>(sc); - } - } - - /// - /// Translate DafnyResolverTag's into IOutliningRegionTag's - /// - internal sealed class OutliningTagger : ITagger - { - ITextBuffer _buffer; - ITextSnapshot _snapshot; // the most recent snapshot of _buffer that we have been informed about - Dafny.Program _program; // the program parsed from _snapshot - List _regions = new List(); // the regions generated from _program - ITagAggregator _aggregator; - - internal OutliningTagger(ITextBuffer buffer, ITagAggregator tagAggregator) { - _buffer = buffer; - _snapshot = _buffer.CurrentSnapshot; - _aggregator = tagAggregator; - _aggregator.TagsChanged += new EventHandler(_aggregator_TagsChanged); - } - - /// - /// Find the Error tokens in the set of all tokens and create an ErrorTag for each - /// - public IEnumerable> GetTags(NormalizedSnapshotSpanCollection spans) { - if (spans.Count == 0) yield break; - // (A NormalizedSnapshotSpanCollection contains spans that all come from the same snapshot.) - // The spans are ordered by the .Start component, and the collection contains no adjacent or abutting spans. - // Hence, to find a span that includes all the ones in "spans", we only need to look at the .Start for the - // first spand and the .End of the last span: - var startPoint = spans[0].Start; - var endPoint = spans[spans.Count - 1].End; - - // Note, (startPoint,endPoint) are points in the spans for which we're being asked to provide tags. We need to translate - // these back into the most recent snapshot that we've computed regions for, namely _snapshot. - var entire = new SnapshotSpan(startPoint, endPoint).TranslateTo(_snapshot, SpanTrackingMode.EdgeExclusive); - int start = entire.Start; - int end = entire.End; - 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( - 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 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 newRegions = new List(); - - 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/Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs b/Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs deleted file mode 100644 index 7fdf38a6..00000000 --- a/Util/VS2010/DafnyExtension/DafnyExtension/ProgressMargin.cs +++ /dev/null @@ -1,260 +0,0 @@ -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 CreateTagger(ITextBuffer buffer) where T : ITag { - ITagAggregator tagAggregator = AggregatorFactory.CreateTagAggregator(buffer); - // create a single tagger for each buffer. - Func> sc = delegate() { return new ProgressTagger(buffer, _serviceProvider, tagAggregator) as ITagger; }; - return buffer.Properties.GetOrCreateSingletonProperty>(sc); - } - } - - internal class ProgressTagger : ITagger - { - ErrorListProvider _errorProvider; - ITextBuffer _buffer; - - readonly DispatcherTimer timer; - - public ProgressTagger(ITextBuffer buffer, IServiceProvider serviceProvider, ITagAggregator 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(_aggregator_TagsChanged); - buffer.Changed += new EventHandler(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 bufferChangesPreVerificationStart = new List(); // buffer changes after the last completed verification and before the currently running verification - List bufferChangesPostVerificationStart = new List(); // 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 - /// - /// 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. - /// - 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(); - } - - /// - /// Thread entry point. - /// - 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(); - 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 TagsChanged; - IEnumerable> ITagger.GetTags(NormalizedSnapshotSpanCollection spans) { - if (spans.Count == 0) yield break; - var targetSnapshot = spans[0].Snapshot; - - List pre; - List 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(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(span, new ProgressGlyphTag(1)); - } - } - - /// - /// (Why the firetruck isn't an extension method like this already in the standard library?) - /// - public static IEnumerable Map(IEnumerable coll, System.Func fn) { - foreach (var e in coll) { - yield return fn(e); - } - } - } -} diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/Properties/AssemblyInfo.cs b/Util/VS2010/DafnyExtension/DafnyExtension/Properties/AssemblyInfo.cs deleted file mode 100644 index b73b8410..00000000 --- a/Util/VS2010/DafnyExtension/DafnyExtension/Properties/AssemblyInfo.cs +++ /dev/null @@ -1,33 +0,0 @@ -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/Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs deleted file mode 100644 index d1af6878..00000000 --- a/Util/VS2010/DafnyExtension/DafnyExtension/ResolverTagger.cs +++ /dev/null @@ -1,321 +0,0 @@ -//*************************************************************************** -// 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 CreateTagger(ITextBuffer buffer) where T : ITag { - // create a single tagger for each buffer. - Func> sc = delegate() { return new ResolverTagger(buffer, _serviceProvider, _textDocumentFactory) as ITagger; }; - return buffer.Properties.GetOrCreateSingletonProperty>(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; - } - } - - /// - /// Translate PkgDefTokenTags into ErrorTags and Error List items - /// - internal sealed class ResolverTagger : ITagger, 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 _resolutionErrors = new List(); // if nonempty, then _snapshot is the snapshot from which the errors were produced - List _verificationErrors = new List(); - 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 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; - } - } - - /// - /// Find the Error tokens in the set of all tokens and create an ErrorTag for each - /// - public IEnumerable> GetTags(NormalizedSnapshotSpanCollection spans) { - if (spans.Count == 0) yield break; - 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(span, new DafnyErrorResolverTag(ty, err.Message)); - } - } - - ITextSnapshot snap; - Dafny.Program prog; - lock (this) { - snap = _snapshot; - prog = _program; - } - if (prog != null) { - yield return new TagSpan(new SnapshotSpan(snap, 0, snap.Length), new DafnySuccessResolverTag(prog)); - } - } - - public event EventHandler TagsChanged; - - /// - /// Calls the Dafny parser/resolver/type checker on the contents of the buffer, updates the Error List accordingly. - /// - 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 : ""); - List newErrors; - Dafny.Program program; - try { - program = driver.ProcessResolution(); - newErrors = driver.Errors; - } catch (Exception e) { - newErrors = new List(); - 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 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; - /// - /// "line" and "col" are expected to be 0-based - /// - 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/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs deleted file mode 100644 index 2f295429..00000000 --- a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs +++ /dev/null @@ -1,342 +0,0 @@ -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 CreateTagger(ITextBuffer buffer) where T : ITag { - return new DafnyTokenTagger(buffer) as ITagger; - } - } - - 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 - { - ITextBuffer _buffer; - ITextSnapshot _snapshot; - List _regions; - - internal DafnyTokenTagger(ITextBuffer buffer) { - _buffer = buffer; - _snapshot = buffer.CurrentSnapshot; - _regions = Rescan(_snapshot); - - _buffer.Changed += new EventHandler(ReparseFile); - } - - public event EventHandler TagsChanged; - - public IEnumerable> GetTags(NormalizedSnapshotSpanCollection spans) { - if (spans.Count == 0) - yield break; - - List 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(new SnapshotSpan(region.Start, region.End), new DafnyTokenTag(region.Kind)); - } - } - } - - /// - /// Find all of the tag regions in the document (snapshot) and notify - /// listeners of any that changed - /// - 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 newRegions = Rescan(snapshot); - - // determine the changed span, and send a changed event with the new spans - List oldSpans = new List(_regions.Select(r => - r.Span.TranslateTo(snapshot, SpanTrackingMode.EdgeExclusive))); - - List newSpans = new List(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 Rescan(ITextSnapshot newSnapshot) { - List newRegions = new List(); - - 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/Util/VS2010/DafnyExtension/DafnyExtension/WordHighlighter.cs b/Util/VS2010/DafnyExtension/DafnyExtension/WordHighlighter.cs deleted file mode 100644 index 03456c85..00000000 --- a/Util/VS2010/DafnyExtension/DafnyExtension/WordHighlighter.cs +++ /dev/null @@ -1,211 +0,0 @@ -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 - { - 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 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 wordSpans = new List(); - //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> 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(currentWord, new HighlightWordTag()); - - // Second, yield all the other words in the file - foreach (SnapshotSpan span in NormalizedSnapshotSpanCollection.Overlap(spans, wordSpans)) { - yield return new TagSpan(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 CreateTagger(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; - } - } -#endregion -#endif -} diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/source.extension.vsixmanifest b/Util/VS2010/DafnyExtension/DafnyExtension/source.extension.vsixmanifest deleted file mode 100644 index ef5c1cf5..00000000 --- a/Util/VS2010/DafnyExtension/DafnyExtension/source.extension.vsixmanifest +++ /dev/null @@ -1,25 +0,0 @@ - - - - DafnyLanguageMode - Microsoft Research - 1.0 - This is a language mode for using the Dafny language inside Visual Studio. - 1033 - - - Pro - - - Pro - - - - - - - |%CurrentProject%| - DafnyPrelude.bpl - UnivBackPred2.smt2 - - -- cgit v1.2.3