diff options
| author |  rustanleino <unknown> | 2010-10-22 01:39:16 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-10-22 01:39:16 +0000 |
| commit | 113fc8a976d5e181ad4a259970c855abff79f644 (patch) | |
| tree | 67acc2cce1647f1be3ec183ad56e932c000a2fbd | |
| parent | 75affe5a214df74d2927785d666fbe3d7871e867 (diff) | |
New Dafny mode for Visual Studio 2010, using the VS2010 extensions.
11 files changed, 1724 insertions, 0 deletions
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension.sln b/Util/VS2010/DafnyExtension/DafnyExtension.sln new file mode 100644 index 00000000..e7391254 --- /dev/null +++ b/Util/VS2010/DafnyExtension/DafnyExtension.sln @@ -0,0 +1,20 @@ +
+Microsoft Visual Studio Solution File, Format Version 11.00
+# Visual Studio 2010
+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 new file mode 100644 index 00000000..44b1affe --- /dev/null +++ b/Util/VS2010/DafnyExtension/DafnyExtension/BraceMatching.cs @@ -0,0 +1,253 @@ +using System;
+using System.Linq;
+using System.Collections.Generic;
+using System.ComponentModel.Composition;
+using Microsoft.VisualStudio.Text;
+using Microsoft.VisualStudio.Text.Editor;
+using Microsoft.VisualStudio.Text.Tagging;
+using Microsoft.VisualStudio.Utilities;
+
+namespace DafnyLanguage
+{
+ [Export(typeof(IViewTaggerProvider))]
+ [ContentType("dafny")]
+ [TagType(typeof(TextMarkerTag))]
+ internal class BraceMatchingTaggerProvider : IViewTaggerProvider
+ {
+ [Import]
+ internal IBufferTagAggregatorFactoryService AggregatorFactory = null;
+
+ public ITagger<T> CreateTagger<T>(ITextView textView, ITextBuffer buffer) where T : ITag {
+ if (textView == null)
+ return null;
+
+ //provide highlighting only on the top-level buffer
+ if (textView.TextBuffer != buffer)
+ return null;
+
+ ITagAggregator<DafnyTokenTag> tagAggregator = AggregatorFactory.CreateTagAggregator<DafnyTokenTag>(buffer);
+ return new BraceMatchingTagger(textView, buffer, tagAggregator) as ITagger<T>;
+ }
+ }
+
+ internal abstract class TokenBasedTagger
+ {
+ ITagAggregator<DafnyTokenTag> _aggregator;
+
+ internal TokenBasedTagger(ITagAggregator<DafnyTokenTag> tagAggregator) {
+ _aggregator = tagAggregator;
+ }
+
+ public bool InsideComment(SnapshotPoint pt) {
+ SnapshotSpan span = new SnapshotSpan(pt, 1);
+ foreach (var tagSpan in this._aggregator.GetTags(span)) {
+ switch (tagSpan.Tag.Kind) {
+ case DafnyTokenKinds.Comment:
+ case DafnyTokenKinds.String:
+ foreach (var s in tagSpan.Span.GetSpans(pt.Snapshot)) {
+ if (s.Contains(span))
+ return true;
+ }
+ break;
+ default:
+ break;
+ }
+ }
+ return false;
+ }
+ }
+
+ internal class BraceMatchingTagger : TokenBasedTagger, ITagger<TextMarkerTag>
+ {
+ ITextView View { get; set; }
+ ITextBuffer SourceBuffer { get; set; }
+ SnapshotPoint? CurrentChar { get; set; }
+ private char[] openBraces;
+ private char[] closeBraces;
+
+ static TextMarkerTag Blue = new TextMarkerTag("blue");
+
+ internal BraceMatchingTagger(ITextView view, ITextBuffer sourceBuffer, ITagAggregator<DafnyTokenTag> tagAggregator)
+ : base(tagAggregator)
+ {
+ //here the keys are the open braces, and the values are the close braces
+ openBraces = new char[] { '(', '{', '[' };
+ closeBraces = new char[] { ')', '}', ']' };
+ this.View = view;
+ this.SourceBuffer = sourceBuffer;
+ this.CurrentChar = null;
+
+ this.View.Caret.PositionChanged += CaretPositionChanged;
+ this.View.LayoutChanged += ViewLayoutChanged;
+ }
+
+ public event EventHandler<SnapshotSpanEventArgs> TagsChanged;
+
+ void ViewLayoutChanged(object sender, TextViewLayoutChangedEventArgs e) {
+ if (e.NewSnapshot != e.OldSnapshot) //make sure that there has really been a change
+ {
+ UpdateAtCaretPosition(View.Caret.Position);
+ }
+ }
+
+ void CaretPositionChanged(object sender, CaretPositionChangedEventArgs e) {
+ UpdateAtCaretPosition(e.NewPosition);
+ }
+
+ void UpdateAtCaretPosition(CaretPosition caretPosition) {
+ CurrentChar = caretPosition.Point.GetPoint(SourceBuffer, caretPosition.Affinity);
+
+ if (!CurrentChar.HasValue)
+ return;
+
+ var chngd = TagsChanged;
+ if (chngd != null)
+ chngd(this, new SnapshotSpanEventArgs(new SnapshotSpan(SourceBuffer.CurrentSnapshot, 0, SourceBuffer.CurrentSnapshot.Length)));
+ }
+
+ public IEnumerable<ITagSpan<TextMarkerTag>> GetTags(NormalizedSnapshotSpanCollection spans) {
+ if (spans.Count == 0) //there is no content in the buffer
+ yield break;
+
+ //don't do anything if the current SnapshotPoint is not initialized
+ if (!CurrentChar.HasValue)
+ yield break;
+
+ //hold on to a snapshot of the current character
+ SnapshotPoint currentChar = CurrentChar.Value;
+
+ //if the requested snapshot isn't the same as the one the brace is on, translate our spans to the expected snapshot
+ if (spans[0].Snapshot != currentChar.Snapshot) {
+ currentChar = currentChar.TranslateTo(spans[0].Snapshot, PointTrackingMode.Positive);
+ }
+
+ if (currentChar.Position < spans[0].Snapshot.Length) {
+ // Check if the current character is an open brace
+ char ch = currentChar.GetChar();
+ char closeCh;
+ if (MatchBrace(currentChar, ch, true, out closeCh)) {
+ SnapshotSpan pairSpan;
+ if (FindMatchingCloseChar(currentChar, ch, closeCh, View.TextViewLines.Count, out pairSpan)) {
+ yield return new TagSpan<TextMarkerTag>(new SnapshotSpan(currentChar, 1), Blue);
+ yield return new TagSpan<TextMarkerTag>(pairSpan, Blue);
+ }
+ }
+ }
+
+ if (0 < currentChar.Position) {
+ // Check if the previous character is a close brace (note, caret may be between a close brace and an open brace, in which case we'll tag two pairs)
+ SnapshotPoint prevChar = currentChar - 1;
+ char ch = prevChar.GetChar();
+ char openCh;
+ if (MatchBrace(prevChar, ch, false, out openCh)) {
+ SnapshotSpan pairSpan;
+ if (FindMatchingOpenChar(prevChar, openCh, ch, View.TextViewLines.Count, out pairSpan)) {
+ yield return new TagSpan<TextMarkerTag>(new SnapshotSpan(prevChar, 1), Blue);
+ yield return new TagSpan<TextMarkerTag>(pairSpan, Blue);
+ }
+ }
+ }
+ }
+
+ private bool MatchBrace(SnapshotPoint pt, char query, bool sourceIsOpen, out char match) {
+ if (!InsideComment(pt)) {
+ char[] source = sourceIsOpen ? openBraces : closeBraces;
+ int i = 0;
+ foreach (char ch in source) {
+ if (ch == query) {
+ char[] dest = sourceIsOpen ? closeBraces : openBraces;
+ match = dest[i];
+ return true;
+ }
+ i++;
+ }
+ }
+ match = query; // satisfy compiler
+ return false;
+ }
+
+ private bool FindMatchingCloseChar(SnapshotPoint startPoint, char open, char close, int linesViewed, out SnapshotSpan pairSpan) {
+ ITextSnapshotLine line = startPoint.GetContainingLine();
+ int lineNumber = line.LineNumber;
+ int offset = startPoint.Position - line.Start.Position + 1;
+
+ int lineNumberLimit = Math.Min(startPoint.Snapshot.LineCount, lineNumber + linesViewed);
+
+ int openCount = 0;
+ while (true) {
+ string lineText = line.GetText();
+
+ //walk the entire line
+ for (; offset < line.Length; offset++) {
+ char currentChar = lineText[offset];
+ if (currentChar == open || currentChar == close) {
+ if (!InsideComment(new SnapshotPoint(line.Snapshot, line.Start.Position + offset))) {
+ if (currentChar == open) {
+ openCount++;
+ } else if (0 < openCount) {
+ openCount--;
+ } else {
+ //found the matching close
+ pairSpan = new SnapshotSpan(startPoint.Snapshot, line.Start + offset, 1);
+ return true;
+ }
+ }
+ }
+ }
+
+ //move on to the next line
+ lineNumber++;
+ if (lineNumberLimit <= lineNumber)
+ break;
+
+ line = line.Snapshot.GetLineFromLineNumber(lineNumber);
+ offset = 0;
+ }
+
+ pairSpan = new SnapshotSpan(startPoint, startPoint); // satisfy the compiler
+ return false;
+ }
+
+ private bool FindMatchingOpenChar(SnapshotPoint startPoint, char open, char close, int linesViewed, out SnapshotSpan pairSpan) {
+ ITextSnapshotLine line = startPoint.GetContainingLine();
+ int lineNumber = line.LineNumber;
+ int offset = startPoint.Position - line.Start.Position - 1; //move the offset to the character before this one
+
+ int lineNumberLimit = Math.Max(0, lineNumber - linesViewed);
+
+ int closeCount = 0;
+ while (true) {
+ string lineText = line.GetText();
+
+ //walk the entire line
+ for (; 0 <= offset; offset--) {
+ char currentChar = lineText[offset];
+ if (currentChar == open || currentChar == close) {
+ if (!InsideComment(new SnapshotPoint(line.Snapshot, line.Start.Position + offset))) {
+ if (currentChar == close) {
+ closeCount++;
+ } else if (0 < closeCount) {
+ closeCount--;
+ } else {
+ // We've found the open character
+ pairSpan = new SnapshotSpan(line.Start + offset, 1); //we just want the character itself
+ return true;
+ }
+ }
+ }
+ }
+
+ // Move to the previous line
+ lineNumber--;
+ if (lineNumber < lineNumberLimit)
+ break;
+
+ line = line.Snapshot.GetLineFromLineNumber(lineNumber);
+ offset = line.Length - 1;
+ }
+
+ pairSpan = new SnapshotSpan(startPoint, startPoint); // satisfy the compiler
+ return false;
+ }
+ }
+}
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/BufferIdleEventUtil.cs b/Util/VS2010/DafnyExtension/DafnyExtension/BufferIdleEventUtil.cs new file mode 100644 index 00000000..1aea1385 --- /dev/null +++ b/Util/VS2010/DafnyExtension/DafnyExtension/BufferIdleEventUtil.cs @@ -0,0 +1,155 @@ +//***************************************************************************
+// Copyright © 2010 Microsoft Corporation. All Rights Reserved.
+// This code released under the terms of the
+// Microsoft Public License (MS-PL, http://opensource.org/licenses/ms-pl.html.)
+//***************************************************************************
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using Microsoft.VisualStudio.Text;
+using System.Windows.Threading;
+
+namespace DafnyLanguage
+{
+ /// <summary>
+ /// Handy reusable utility to listen for change events on the associated buffer, but
+ /// only pass these along to a set of listeners when the user stops typing for a half second
+ /// </summary>
+ static class BufferIdleEventUtil
+ {
+ static object bufferListenersKey = new object();
+ static object bufferTimerKey = new object();
+
+ #region Public interface
+
+ public static bool AddBufferIdleEventListener(ITextBuffer buffer, EventHandler handler)
+ {
+ HashSet<EventHandler> listenersForBuffer;
+ if (!TryGetBufferListeners(buffer, out listenersForBuffer))
+ listenersForBuffer = ConnectToBuffer(buffer);
+
+ if (listenersForBuffer.Contains(handler))
+ return false;
+
+ listenersForBuffer.Add(handler);
+
+ return true;
+ }
+
+ public static bool RemoveBufferIdleEventListener(ITextBuffer buffer, EventHandler handler)
+ {
+ HashSet<EventHandler> listenersForBuffer;
+ if (!TryGetBufferListeners(buffer, out listenersForBuffer))
+ return false;
+
+ if (!listenersForBuffer.Contains(handler))
+ return false;
+
+ listenersForBuffer.Remove(handler);
+
+ if (listenersForBuffer.Count == 0)
+ DisconnectFromBuffer(buffer);
+
+ return true;
+ }
+
+ #endregion
+
+ #region Helpers
+
+ static bool TryGetBufferListeners(ITextBuffer buffer, out HashSet<EventHandler> listeners)
+ {
+ return buffer.Properties.TryGetProperty(bufferListenersKey, out listeners);
+ }
+
+ static void ClearBufferListeners(ITextBuffer buffer)
+ {
+ buffer.Properties.RemoveProperty(bufferListenersKey);
+ }
+
+ static bool TryGetBufferTimer(ITextBuffer buffer, out DispatcherTimer timer)
+ {
+ return buffer.Properties.TryGetProperty(bufferTimerKey, out timer);
+ }
+
+ static void ClearBufferTimer(ITextBuffer buffer)
+ {
+ DispatcherTimer timer;
+ if (TryGetBufferTimer(buffer, out timer))
+ {
+ if (timer != null)
+ timer.Stop();
+ buffer.Properties.RemoveProperty(bufferTimerKey);
+ }
+ }
+
+ static void DisconnectFromBuffer(ITextBuffer buffer)
+ {
+ buffer.Changed -= BufferChanged;
+
+ ClearBufferListeners(buffer);
+ ClearBufferTimer(buffer);
+
+ buffer.Properties.RemoveProperty(bufferListenersKey);
+ }
+
+ static HashSet<EventHandler> ConnectToBuffer(ITextBuffer buffer)
+ {
+ buffer.Changed += BufferChanged;
+
+ RestartTimerForBuffer(buffer);
+
+ HashSet<EventHandler> listenersForBuffer = new HashSet<EventHandler>();
+ buffer.Properties[bufferListenersKey] = listenersForBuffer;
+
+ return listenersForBuffer;
+ }
+
+ static void RestartTimerForBuffer(ITextBuffer buffer)
+ {
+ DispatcherTimer timer;
+
+ if (TryGetBufferTimer(buffer, out timer))
+ {
+ timer.Stop();
+ }
+ else
+ {
+ timer = new DispatcherTimer(DispatcherPriority.ApplicationIdle)
+ {
+ Interval = TimeSpan.FromMilliseconds(500)
+ };
+
+ timer.Tick += (s, e) =>
+ {
+ ClearBufferTimer(buffer);
+
+ HashSet<EventHandler> handlers;
+ if (TryGetBufferListeners(buffer, out handlers))
+ {
+ foreach (var handler in handlers)
+ {
+ handler(buffer, new EventArgs());
+ }
+ }
+ };
+
+ buffer.Properties[bufferTimerKey] = timer;
+ }
+
+ timer.Start();
+ }
+
+ static void BufferChanged(object sender, TextContentChangedEventArgs e)
+ {
+ ITextBuffer buffer = sender as ITextBuffer;
+ if (buffer == null)
+ return;
+
+ RestartTimerForBuffer(buffer);
+ }
+
+ #endregion
+ }
+}
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/ClassificationTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/ClassificationTagger.cs new file mode 100644 index 00000000..98bb7033 --- /dev/null +++ b/Util/VS2010/DafnyExtension/DafnyExtension/ClassificationTagger.cs @@ -0,0 +1,136 @@ +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;
+
+ public ITagger<T> CreateTagger<T>(ITextBuffer buffer) where T : ITag {
+ ITagAggregator<DafnyTokenTag> tagAggregator = AggregatorFactory.CreateTagAggregator<DafnyTokenTag>(buffer);
+ return new DafnyClassifier(buffer, tagAggregator, ClassificationTypeRegistry) 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) {
+ _buffer = buffer;
+ _aggregator = tagAggregator;
+ _aggregator.TagsChanged += new EventHandler<TagsChangedEventArgs>(_aggregator_TagsChanged);
+ _typeMap = new Dictionary<DafnyTokenKinds, IClassificationType>();
+ _typeMap[DafnyTokenKinds.Keyword] = typeService.GetClassificationType("keyword"); // use the built-in "keyword" classification type
+ _typeMap[DafnyTokenKinds.Number] = typeService.GetClassificationType("number"); // use the built-in "number" classification type
+ _typeMap[DafnyTokenKinds.String] = typeService.GetClassificationType("string"); // use the built-in "string" classification type
+ _typeMap[DafnyTokenKinds.Comment] = typeService.GetClassificationType("comment"); // use the built-in "comment" classification type
+ }
+
+ 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));
+ }
+ }
+ }
+ }
+
+#if false // the commented-out code here shows show to define new classifier types; however, the Dafny mode just uses the built-in "keyword" and "number" classifier types
+ /// <summary>
+ /// Defines an editor format for the keyword type.
+ /// </summary>
+ [Export(typeof(EditorFormatDefinition))]
+ [ClassificationType(ClassificationTypeNames = "Dafny-keyword")]
+ [Name("Dafny-keyword")]
+ //this should be visible to the end user
+ [UserVisible(false)]
+ //set the priority to be after the default classifiers
+ [Order(Before = Priority.Default)]
+ internal sealed class Keyword : ClassificationFormatDefinition
+ {
+ /// <summary>
+ /// Defines the visual format for the "ordinary" classification type
+ /// </summary>
+ public Keyword() {
+ this.DisplayName = "Dafny keyword"; //human readable version of the name
+ this.ForegroundColor = Colors.BlueViolet;
+ }
+ }
+
+ /// <summary>
+ /// Defines an editor format for the OrdinaryClassification type that has a purple background
+ /// and is underlined.
+ /// </summary>
+ [Export(typeof(EditorFormatDefinition))]
+ [ClassificationType(ClassificationTypeNames = "Dafny-number")]
+ [Name("Dafny-number")]
+ //this should be visible to the end user
+ [UserVisible(false)]
+ //set the priority to be after the default classifiers
+ [Order(Before = Priority.Default)]
+ internal sealed class Number : ClassificationFormatDefinition
+ {
+ /// <summary>
+ /// Defines the visual format for the "ordinary" classification type
+ /// </summary>
+ public Number() {
+ this.DisplayName = "Dafny numeric literal"; //human readable version of the name
+ this.ForegroundColor = Colors.Orange;
+ }
+ }
+
+ internal static class ClassificationDefinition
+ {
+ /// <summary>
+ /// Defines the "ordinary" classification type.
+ /// </summary>
+ [Export(typeof(ClassificationTypeDefinition))]
+ [Name("Dafny-keyword")]
+ internal static ClassificationTypeDefinition Keyword = null;
+
+ /// <summary>
+ /// Defines the "ordinary" classification type.
+ /// </summary>
+ [Export(typeof(ClassificationTypeDefinition))]
+ [Name("Dafny-number")]
+ internal static ClassificationTypeDefinition Number = null;
+ }
+#endif
+}
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/ContentType.cs b/Util/VS2010/DafnyExtension/DafnyExtension/ContentType.cs new file mode 100644 index 00000000..d8487f74 --- /dev/null +++ b/Util/VS2010/DafnyExtension/DafnyExtension/ContentType.cs @@ -0,0 +1,18 @@ +using System.ComponentModel.Composition;
+using Microsoft.VisualStudio.Utilities;
+
+namespace DafnyLanguage
+{
+ class DafnyContentType
+ {
+ [Export]
+ [Name("dafny")]
+ [BaseDefinition("code")]
+ internal static ContentTypeDefinition ContentType = null;
+
+ [Export]
+ [FileExtension(".dfy")]
+ [ContentType("dafny")]
+ internal static FileExtensionToContentTypeDefinition FileType = null;
+ }
+}
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj new file mode 100644 index 00000000..f6320284 --- /dev/null +++ b/Util/VS2010/DafnyExtension/DafnyExtension/DafnyExtension.csproj @@ -0,0 +1,108 @@ +<?xml version="1.0" encoding="utf-8"?>
+<Project ToolsVersion="4.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
+ <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>
+ </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="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="ContentType.cs" />
+ <Compile Include="BraceMatching.cs" />
+ <Compile Include="WordHighlighter.cs" />
+ <Compile Include="Outlining.cs" />
+ <Compile Include="ErrorTagger.cs" />
+ <Compile Include="TokenTagger.cs" />
+ <Compile Include="ClassificationTagger.cs" />
+ <Compile Include="Properties\AssemblyInfo.cs" />
+ </ItemGroup>
+ <ItemGroup>
+ <None Include="source.extension.vsixmanifest">
+ <SubType>Designer</SubType>
+ </None>
+ </ItemGroup>
+ <ItemGroup>
+ <WCFMetadata Include="Service References\" />
+ </ItemGroup>
+ <Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />
+ <Import Project="$(MSBuildExtensionsPath)\Microsoft\VisualStudio\v10.0\VSSDK\Microsoft.VsSDK.targets" />
+ <!-- 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 new file mode 100644 index 00000000..393aa8c8 --- /dev/null +++ b/Util/VS2010/DafnyExtension/DafnyExtension/ErrorTagger.cs @@ -0,0 +1,255 @@ +//***************************************************************************
+// 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;
+using System.IO;
+
+namespace DafnyLanguage
+{
+ [Export(typeof(ITaggerProvider))]
+ [ContentType("dafny")]
+ [TagType(typeof(ErrorTag))]
+ internal sealed class ErrorTaggerProvider : 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 ErrorTagger(buffer, _serviceProvider, _textDocumentFactory) 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>, IDisposable
+ {
+ ITextBuffer _buffer;
+ ITextDocument _document;
+ ITextSnapshot _snapshot; // may be null
+ List<DafnyError> _errors = new List<DafnyError>();
+ ErrorListProvider _errorProvider;
+
+ internal ErrorTagger(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);
+
+ // ProcessFile(null, EventArgs.Empty);
+ BufferIdleEventUtil.AddBufferIdleEventListener(_buffer, ProcessFile);
+ }
+
+ public void Dispose() {
+ if (_errorProvider != null) {
+ _errorProvider.Tasks.Clear();
+ _errorProvider.Dispose();
+ }
+ BufferIdleEventUtil.RemoveBufferIdleEventListener(_buffer, ProcessFile);
+ }
+
+ /// <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 err in _errors) {
+ if (err.Category != ErrorCategory.ProcessError) {
+ var line = snapshot.GetLineFromLineNumber(err.Line);
+ var length = line.Length - err.Column;
+ if (5 < length) length = 5;
+ SnapshotSpan span = new SnapshotSpan(new SnapshotPoint(snapshot, line.Start.Position + err.Column), length);
+ // http://msdn.microsoft.com/en-us/library/dd885244.aspx says one can use the error types below, but they
+ // all show as purple squiggles for me. And just "error" (which is not mentioned on that page) shows up
+ // as red.
+ string ty;
+ switch (err.Category) {
+ default: // unexpected category
+ case ErrorCategory.ParseError:
+ // ty = "syntax error";
+ ty = "error"; break;
+ case ErrorCategory.ResolveError:
+ ty = "compiler error"; break;
+ case ErrorCategory.VerificationError:
+ ty = "other error"; break;
+ }
+ yield return new TagSpan<ErrorTag>(span, new ErrorTag(ty, err.Message));
+ }
+ }
+ }
+
+ // the Classifier tagger is translating buffer change events into TagsChanged events, so we don't have to
+ public event EventHandler<SnapshotSpanEventArgs> TagsChanged;
+
+ /// <summary>
+ /// Calls the Dafny verifier on the program, updates the Error List accordingly.
+ /// </summary>
+ void ProcessFile(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 newErrors = Verify(_buffer.CurrentSnapshot.GetText());
+
+ _errorProvider.Tasks.Clear();
+ foreach (var err in newErrors) {
+ ErrorTask task = new ErrorTask();
+ task.CanDelete = true;
+ task.Category = TaskCategory.BuildCompile;
+ if (_document != null)
+ task.Document = _document.FilePath;
+ task.ErrorCategory = TaskErrorCategory.Error;
+ task.Text = err.Message;
+ if (err.Category != ErrorCategory.ProcessError) {
+ task.Line = err.Line;
+ task.Column = err.Column;
+ task.Navigate += new EventHandler(task_Navigate);
+ }
+ _errorProvider.Tasks.Add(task);
+ }
+
+ _errors = newErrors;
+ _snapshot = snapshot;
+ var chng = TagsChanged;
+ if (chng != null)
+ chng(this, new SnapshotSpanEventArgs(new SnapshotSpan(snapshot, 0, snapshot.Length)));
+ }
+
+ private static List<DafnyError> Verify(string theProgram) {
+ List<DafnyError> errors = new List<DafnyError>();
+
+ if (!File.Exists(@"C:\tmp\StartDafny.bat")) {
+ RecordError(errors, 0, 0, ErrorCategory.ProcessError, @"Can't find C:\tmp\StartDafny.bat");
+ return errors;
+ }
+
+ // From: http://dotnetperls.com/process-redirect-standard-output
+ // (Also, see: http://msdn.microsoft.com/en-us/library/system.diagnostics.processstartinfo.redirectstandardoutput.aspx)
+ //
+ // Setup the process with the ProcessStartInfo class.
+ //
+ ProcessStartInfo start = new ProcessStartInfo();
+ start.FileName = @"cmd.exe";
+ start.Arguments = @"/c C:\tmp\StartDafny.bat"; // Specify exe name.
+ start.UseShellExecute = false;
+ start.RedirectStandardInput = true;
+ start.RedirectStandardOutput = true;
+ start.CreateNoWindow = true;
+ //
+ // Start the process.
+ //
+ using (System.Diagnostics.Process process = System.Diagnostics.Process.Start(start)) {
+ //
+ // Push the file contents to the new process
+ //
+ StreamWriter myStreamWriter = process.StandardInput;
+ myStreamWriter.WriteLine(theProgram);
+ myStreamWriter.Close();
+ //
+ // Read in all the text from the process with the StreamReader.
+ //
+ using (StreamReader reader = process.StandardOutput) {
+ for (string line = reader.ReadLine(); !String.IsNullOrEmpty(line); line = reader.ReadLine()) {
+ // the lines of interest have the form "filename(line,col): some_error_label: error_message"
+ // where "some_error_label" is "Error" or "syntax error" or "Error BP5003" or "Related location"
+ string message;
+ int n = line.IndexOf("): ", 2); // we start at 2, to avoid problems with "C:\..."
+ if (n == -1) {
+ continue;
+ } else {
+ int m = line.IndexOf(": ", n + 3);
+ if (m == -1) {
+ continue;
+ }
+ message = line.Substring(m + 2);
+ }
+ line = line.Substring(0, n); // line now has the form "filename(line,col"
+
+ n = line.LastIndexOf(',');
+ if (n == -1) { continue; }
+ var colString = line.Substring(n + 1);
+ line = line.Substring(0, n); // line now has the form "filename(line"
+
+ n = line.LastIndexOf('(');
+ if (n == -1) { continue; }
+ var lineString = line.Substring(n + 1);
+
+ try {
+ int errLine = Int32.Parse(lineString) - 1;
+ int errCol = Int32.Parse(colString) - 1;
+ RecordError(errors, errLine, errCol, message.StartsWith("syntax error") ? ErrorCategory.ParseError : ErrorCategory.VerificationError, message);
+ } catch (System.FormatException) {
+ continue;
+ } catch (System.OverflowException) {
+ continue;
+ }
+ }
+ }
+ }
+ return errors;
+ }
+
+ private static void RecordError(List<DafnyError> errors, int line, int col, ErrorCategory cat, string msg) {
+ errors.Add(new DafnyError(line, col, cat, msg));
+ }
+
+ /// <summary>
+ /// Callback method attached to each of our tasks in the Error List
+ /// </summary>
+ void task_Navigate(object sender, EventArgs e) {
+ ErrorTask error = sender as ErrorTask;
+ if (error != null) {
+ error.Line += 1;
+ error.Column += 1;
+ _errorProvider.Navigate(error, new Guid(EnvDTE.Constants.vsViewKindCode));
+ error.Column -= 1;
+ error.Line -= 1;
+ }
+ }
+ }
+
+ public enum ErrorCategory
+ {
+ ProcessError, ParseError, ResolveError, VerificationError
+ }
+
+ internal class DafnyError
+ {
+ public readonly int Line; // 0 based
+ public readonly int Column; // 0 based
+ public readonly ErrorCategory Category;
+ public readonly string Message;
+ public DafnyError(int line, int col, ErrorCategory cat, string msg) {
+ Line = line;
+ Column = col;
+ Category = cat;
+ Message = msg;
+ }
+ }
+}
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/Outlining.cs b/Util/VS2010/DafnyExtension/DafnyExtension/Outlining.cs new file mode 100644 index 00000000..3fbcb054 --- /dev/null +++ b/Util/VS2010/DafnyExtension/DafnyExtension/Outlining.cs @@ -0,0 +1,220 @@ +using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Text.RegularExpressions;
+using System.Windows.Threading;
+using System.ComponentModel.Composition;
+using Microsoft.VisualStudio.Text.Outlining;
+using Microsoft.VisualStudio.Text.Tagging;
+using Microsoft.VisualStudio.Utilities;
+using Microsoft.VisualStudio.Text;
+
+namespace DafnyLanguage
+{
+ [Export(typeof(ITaggerProvider))]
+ [ContentType("dafny")]
+ [TagType(typeof(IOutliningRegionTag))]
+ internal sealed class OutliningTaggerProvider : ITaggerProvider
+ {
+ public ITagger<T> CreateTagger<T>(ITextBuffer buffer) where T : ITag {
+ // create a single tagger for each buffer.
+ Func<ITagger<T>> sc = delegate() { return new OutlineTagger(buffer) as ITagger<T>; };
+ return buffer.Properties.GetOrCreateSingletonProperty<ITagger<T>>(sc);
+ }
+ }
+
+ /// <summary>
+ /// Data about one outline region
+ /// </summary>
+ internal class OutlineRegion
+ {
+ public SnapshotPoint Start { get; set; }
+ public SnapshotPoint End { get; set; }
+ public SnapshotSpan Span {
+ get { return new SnapshotSpan(Start, End); }
+ }
+
+ public string HoverText { get; set; }
+ public string Label { get; set; }
+ }
+
+ internal sealed class OutlineTagger : ITagger<IOutliningRegionTag>
+ {
+ ITextBuffer _buffer;
+ ITextSnapshot _snapshot;
+ List<OutlineRegion> _regions;
+
+ public OutlineTagger(ITextBuffer buffer) {
+ _buffer = buffer;
+ _snapshot = buffer.CurrentSnapshot;
+ _regions = new List<OutlineRegion>();
+
+ ReparseFile(null, EventArgs.Empty);
+
+ // listen for changes to the buffer, but don't process until the user stops typing
+ BufferIdleEventUtil.AddBufferIdleEventListener(_buffer, ReparseFile);
+ }
+
+ public void Dispose() {
+ BufferIdleEventUtil.RemoveBufferIdleEventListener(_buffer, ReparseFile);
+ }
+
+ public IEnumerable<ITagSpan<IOutliningRegionTag>> GetTags(NormalizedSnapshotSpanCollection spans) {
+ if (spans.Count == 0)
+ yield break;
+
+ List<OutlineRegion> 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);
+ int startLineNumber = entire.Start.GetContainingLine().LineNumber;
+ int endLineNumber = entire.End.GetContainingLine().LineNumber;
+
+ // return outline tags for any regions that fall within that span
+ foreach (var region in currentRegions) {
+ if (entire.IntersectsWith(region.Span)) {
+ //the region starts at the beginning of the "{", and goes until the *end* of the line that contains the "}".
+ yield return new TagSpan<OutliningRegionTag>(new SnapshotSpan(region.Start, region.End),
+ new OutliningRegionTag(false, false, region.Label, region.HoverText));
+ }
+ }
+ }
+
+ public event EventHandler<SnapshotSpanEventArgs> TagsChanged;
+
+ static string ellipsis = "..."; //the characters that are displayed when the region is collapsed
+ static Regex matchKey = new Regex("^\\s*(datatype|method|function)");
+ static int MaxHiddenLines = 15;
+ static char[] eitherBrace = { '{', '}' };
+
+ /// <summary>
+ /// Find all of the outline sections in the snapshot
+ /// </summary>
+ private List<OutlineRegion> ParseOutlineSections(ITextSnapshot newSnapshot) {
+ List<OutlineRegion> newRegions = new List<OutlineRegion>();
+
+ // We care about three states:
+ // (0) looking for an outlineable declaration
+ // (1) have found an outlineable declaration, looking for an open curly
+ // (2) looking for a close curly
+ // The search used here is not at all exact, and it would be easy to get it to
+ // do the wrong thing; however, in common cases, it will do the right thing.
+ int state = 0;
+ SnapshotPoint start = new SnapshotPoint(); // the value of "start" matters only if state==2
+ int braceImbalance = 0; // used only if state==2
+ string hoverText = ""; // used only if state==2
+ int hoverLineCount = 0; // used only if state==2
+ string prevLineBreak = ""; // used only if state==2
+ foreach (ITextSnapshotLine line in newSnapshot.Lines) {
+ string txt = line.GetText();
+ if (state == 0) {
+ MatchCollection matches = matchKey.Matches(txt);
+ if (matches.Count != 0)
+ state = 1;
+ }
+ int startPos = 0;
+ if (state == 1) {
+ startPos = txt.IndexOf('{');
+ if (startPos != -1) {
+ start = new SnapshotPoint(newSnapshot, line.Start.Position + startPos + 1);
+ startPos++;
+ state = 2;
+ braceImbalance = 1;
+ hoverText = txt.Substring(startPos).Trim();
+ hoverLineCount = hoverText.Length == 0 ? 0 : 1;
+ prevLineBreak = line.GetLineBreakText();
+ }
+ }
+ if (state == 2) {
+ int endPos = startPos;
+ while (braceImbalance != 0) {
+ endPos = txt.IndexOfAny(eitherBrace, endPos);
+ if (endPos == -1) break;
+ char ch = txt[endPos];
+ if (ch == '{') {
+ braceImbalance++;
+ } else {
+ braceImbalance--;
+ if (braceImbalance == 0) break;
+ }
+ endPos++;
+ }
+
+ if (endPos == -1) {
+ // not there yet
+ if (startPos == 0 && hoverLineCount < MaxHiddenLines) {
+ string h = txt.Trim();
+ if (h.Length != 0) {
+ if (hoverText.Length != 0)
+ hoverText += prevLineBreak;
+ hoverText += h;
+ hoverLineCount++;
+ prevLineBreak = line.GetLineBreakText();
+ }
+ }
+ } else {
+ // we found the end
+ if (startPos != 0) {
+ hoverText = txt.Substring(startPos, endPos - startPos).Trim();
+ } else if (hoverLineCount < MaxHiddenLines) {
+ string h = txt.Substring(0, endPos).Trim();
+ if (h.Length != 0) {
+ if (hoverText.Length != 0)
+ hoverText += prevLineBreak;
+ hoverText += h;
+ }
+ }
+ SnapshotPoint end = new SnapshotPoint(newSnapshot, line.Start.Position + endPos);
+ newRegions.Add(new OutlineRegion() {
+ Start = start, End = end, Label = ellipsis,
+ HoverText = hoverText
+ });
+ state = 0;
+ }
+ }
+ }
+
+ return newRegions;
+ }
+
+ /// <summary>
+ /// Find all of the outline regions in the document (snapshot) and notify
+ /// listeners of any that changed
+ /// </summary>
+ void ReparseFile(object sender, EventArgs args) {
+ ITextSnapshot snapshot = _buffer.CurrentSnapshot;
+
+ // get all of the outline regions in the snapshot
+ List<OutlineRegion> newRegions = ParseOutlineSections(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;
+
+ foreach (var span in difference) {
+ var chng = TagsChanged;
+ if (chng != null)
+ chng(this, new SnapshotSpanEventArgs(span));
+ }
+ }
+
+ NormalizedSnapshotSpanCollection SymmetricDifference(NormalizedSnapshotSpanCollection first, NormalizedSnapshotSpanCollection second) {
+ return NormalizedSnapshotSpanCollection.Union(
+ NormalizedSnapshotSpanCollection.Difference(first, second),
+ NormalizedSnapshotSpanCollection.Difference(second, first));
+ }
+ }
+}
diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs new file mode 100644 index 00000000..9b0e5025 --- /dev/null +++ b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs @@ -0,0 +1,327 @@ +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;
+
+
+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
+ }
+
+ public class DafnyTokenTag : ITag
+ {
+ public DafnyTokenKinds Kind { get; private set; }
+
+ public DafnyTokenTag(DafnyTokenKinds kind) {
+ this.Kind = kind;
+ }
+ }
+
+ 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);
+ int startLineNumber = entire.Start.GetContainingLine().LineNumber;
+ int endLineNumber = entire.End.GetContainingLine().LineNumber;
+
+ // 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)) {
+ // BUGBUG: this returns a span for currentSnapshot, but shouldn't we return spans for the spans[0].Snapshot?
+ 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;
+
+ foreach (var span in difference) {
+ var chng = TagsChanged;
+ if (chng != null)
+ 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' && s != "array1") {
+ // this is a keyword (array2, array3, ...)
+ } else {
+ switch (s) {
+ #region keywords
+ case "array":
+ case "assert":
+ case "assume":
+ case "bool":
+ case "break":
+ case "by":
+ case "call":
+ case "case":
+ case "class":
+ case "datatype":
+ case "decreases":
+ case "else":
+ case "ensures":
+ case "exists":
+ case "false":
+ case "forall":
+ case "foreach":
+ case "free":
+ case "fresh":
+ case "function":
+ case "ghost":
+ case "havoc":
+ case "if":
+ case "imports":
+ case "in":
+ case "int":
+ case "invariant":
+ case "label":
+ case "match":
+ case "method":
+ case "modifies":
+ case "module":
+ case "new":
+ case "null":
+ case "object":
+ case "old":
+ case "print":
+ case "reads":
+ case "refines":
+ case "replaces":
+ case "requires":
+ case "return":
+ case "returns":
+ case "seq":
+ case "set":
+ case "static":
+ case "then":
+ case "this":
+ case "true":
+ case "unlimited":
+ case "use":
+ case "var":
+ case "while":
+ #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 new file mode 100644 index 00000000..3677671a --- /dev/null +++ b/Util/VS2010/DafnyExtension/DafnyExtension/WordHighlighter.cs @@ -0,0 +1,212 @@ +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 false
+ #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
+ && point.Value >= CurrentWord.Value.Start
+ && 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 new file mode 100644 index 00000000..35e8f1f9 --- /dev/null +++ b/Util/VS2010/DafnyExtension/DafnyExtension/source.extension.vsixmanifest @@ -0,0 +1,20 @@ +<?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>
+ </SupportedProducts>
+ <SupportedFrameworkRuntimeEdition MinVersion="4.0" MaxVersion="4.0" />
+ </Identifier>
+ <References />
+ <Content>
+ <MefComponent>|%CurrentProject%|</MefComponent>
+ </Content>
+</Vsix>
|