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