diff options
Diffstat (limited to 'Source/DafnyExtension/BraceMatching.cs')
| -rw-r--r-- | Source/DafnyExtension/BraceMatching.cs | 253 |
1 files changed, 253 insertions, 0 deletions
diff --git a/Source/DafnyExtension/BraceMatching.cs b/Source/DafnyExtension/BraceMatching.cs new file mode 100644 index 00000000..44b1affe --- /dev/null +++ b/Source/DafnyExtension/BraceMatching.cs @@ -0,0 +1,253 @@ +using System;
+using System.Linq;
+using System.Collections.Generic;
+using System.ComponentModel.Composition;
+using Microsoft.VisualStudio.Text;
+using Microsoft.VisualStudio.Text.Editor;
+using Microsoft.VisualStudio.Text.Tagging;
+using Microsoft.VisualStudio.Utilities;
+
+namespace DafnyLanguage
+{
+ [Export(typeof(IViewTaggerProvider))]
+ [ContentType("dafny")]
+ [TagType(typeof(TextMarkerTag))]
+ internal class BraceMatchingTaggerProvider : IViewTaggerProvider
+ {
+ [Import]
+ internal IBufferTagAggregatorFactoryService AggregatorFactory = null;
+
+ public ITagger<T> CreateTagger<T>(ITextView textView, ITextBuffer buffer) where T : ITag {
+ if (textView == null)
+ return null;
+
+ //provide highlighting only on the top-level buffer
+ if (textView.TextBuffer != buffer)
+ return null;
+
+ ITagAggregator<DafnyTokenTag> tagAggregator = AggregatorFactory.CreateTagAggregator<DafnyTokenTag>(buffer);
+ return new BraceMatchingTagger(textView, buffer, tagAggregator) as ITagger<T>;
+ }
+ }
+
+ internal abstract class TokenBasedTagger
+ {
+ ITagAggregator<DafnyTokenTag> _aggregator;
+
+ internal TokenBasedTagger(ITagAggregator<DafnyTokenTag> tagAggregator) {
+ _aggregator = tagAggregator;
+ }
+
+ public bool InsideComment(SnapshotPoint pt) {
+ SnapshotSpan span = new SnapshotSpan(pt, 1);
+ foreach (var tagSpan in this._aggregator.GetTags(span)) {
+ switch (tagSpan.Tag.Kind) {
+ case DafnyTokenKinds.Comment:
+ case DafnyTokenKinds.String:
+ foreach (var s in tagSpan.Span.GetSpans(pt.Snapshot)) {
+ if (s.Contains(span))
+ return true;
+ }
+ break;
+ default:
+ break;
+ }
+ }
+ return false;
+ }
+ }
+
+ internal class BraceMatchingTagger : TokenBasedTagger, ITagger<TextMarkerTag>
+ {
+ ITextView View { get; set; }
+ ITextBuffer SourceBuffer { get; set; }
+ SnapshotPoint? CurrentChar { get; set; }
+ private char[] openBraces;
+ private char[] closeBraces;
+
+ static TextMarkerTag Blue = new TextMarkerTag("blue");
+
+ internal BraceMatchingTagger(ITextView view, ITextBuffer sourceBuffer, ITagAggregator<DafnyTokenTag> tagAggregator)
+ : base(tagAggregator)
+ {
+ //here the keys are the open braces, and the values are the close braces
+ openBraces = new char[] { '(', '{', '[' };
+ closeBraces = new char[] { ')', '}', ']' };
+ this.View = view;
+ this.SourceBuffer = sourceBuffer;
+ this.CurrentChar = null;
+
+ this.View.Caret.PositionChanged += CaretPositionChanged;
+ this.View.LayoutChanged += ViewLayoutChanged;
+ }
+
+ public event EventHandler<SnapshotSpanEventArgs> TagsChanged;
+
+ void ViewLayoutChanged(object sender, TextViewLayoutChangedEventArgs e) {
+ if (e.NewSnapshot != e.OldSnapshot) //make sure that there has really been a change
+ {
+ UpdateAtCaretPosition(View.Caret.Position);
+ }
+ }
+
+ void CaretPositionChanged(object sender, CaretPositionChangedEventArgs e) {
+ UpdateAtCaretPosition(e.NewPosition);
+ }
+
+ void UpdateAtCaretPosition(CaretPosition caretPosition) {
+ CurrentChar = caretPosition.Point.GetPoint(SourceBuffer, caretPosition.Affinity);
+
+ if (!CurrentChar.HasValue)
+ return;
+
+ var chngd = TagsChanged;
+ if (chngd != null)
+ chngd(this, new SnapshotSpanEventArgs(new SnapshotSpan(SourceBuffer.CurrentSnapshot, 0, SourceBuffer.CurrentSnapshot.Length)));
+ }
+
+ public IEnumerable<ITagSpan<TextMarkerTag>> GetTags(NormalizedSnapshotSpanCollection spans) {
+ if (spans.Count == 0) //there is no content in the buffer
+ yield break;
+
+ //don't do anything if the current SnapshotPoint is not initialized
+ if (!CurrentChar.HasValue)
+ yield break;
+
+ //hold on to a snapshot of the current character
+ SnapshotPoint currentChar = CurrentChar.Value;
+
+ //if the requested snapshot isn't the same as the one the brace is on, translate our spans to the expected snapshot
+ if (spans[0].Snapshot != currentChar.Snapshot) {
+ currentChar = currentChar.TranslateTo(spans[0].Snapshot, PointTrackingMode.Positive);
+ }
+
+ if (currentChar.Position < spans[0].Snapshot.Length) {
+ // Check if the current character is an open brace
+ char ch = currentChar.GetChar();
+ char closeCh;
+ if (MatchBrace(currentChar, ch, true, out closeCh)) {
+ SnapshotSpan pairSpan;
+ if (FindMatchingCloseChar(currentChar, ch, closeCh, View.TextViewLines.Count, out pairSpan)) {
+ yield return new TagSpan<TextMarkerTag>(new SnapshotSpan(currentChar, 1), Blue);
+ yield return new TagSpan<TextMarkerTag>(pairSpan, Blue);
+ }
+ }
+ }
+
+ if (0 < currentChar.Position) {
+ // Check if the previous character is a close brace (note, caret may be between a close brace and an open brace, in which case we'll tag two pairs)
+ SnapshotPoint prevChar = currentChar - 1;
+ char ch = prevChar.GetChar();
+ char openCh;
+ if (MatchBrace(prevChar, ch, false, out openCh)) {
+ SnapshotSpan pairSpan;
+ if (FindMatchingOpenChar(prevChar, openCh, ch, View.TextViewLines.Count, out pairSpan)) {
+ yield return new TagSpan<TextMarkerTag>(new SnapshotSpan(prevChar, 1), Blue);
+ yield return new TagSpan<TextMarkerTag>(pairSpan, Blue);
+ }
+ }
+ }
+ }
+
+ private bool MatchBrace(SnapshotPoint pt, char query, bool sourceIsOpen, out char match) {
+ if (!InsideComment(pt)) {
+ char[] source = sourceIsOpen ? openBraces : closeBraces;
+ int i = 0;
+ foreach (char ch in source) {
+ if (ch == query) {
+ char[] dest = sourceIsOpen ? closeBraces : openBraces;
+ match = dest[i];
+ return true;
+ }
+ i++;
+ }
+ }
+ match = query; // satisfy compiler
+ return false;
+ }
+
+ private bool FindMatchingCloseChar(SnapshotPoint startPoint, char open, char close, int linesViewed, out SnapshotSpan pairSpan) {
+ ITextSnapshotLine line = startPoint.GetContainingLine();
+ int lineNumber = line.LineNumber;
+ int offset = startPoint.Position - line.Start.Position + 1;
+
+ int lineNumberLimit = Math.Min(startPoint.Snapshot.LineCount, lineNumber + linesViewed);
+
+ int openCount = 0;
+ while (true) {
+ string lineText = line.GetText();
+
+ //walk the entire line
+ for (; offset < line.Length; offset++) {
+ char currentChar = lineText[offset];
+ if (currentChar == open || currentChar == close) {
+ if (!InsideComment(new SnapshotPoint(line.Snapshot, line.Start.Position + offset))) {
+ if (currentChar == open) {
+ openCount++;
+ } else if (0 < openCount) {
+ openCount--;
+ } else {
+ //found the matching close
+ pairSpan = new SnapshotSpan(startPoint.Snapshot, line.Start + offset, 1);
+ return true;
+ }
+ }
+ }
+ }
+
+ //move on to the next line
+ lineNumber++;
+ if (lineNumberLimit <= lineNumber)
+ break;
+
+ line = line.Snapshot.GetLineFromLineNumber(lineNumber);
+ offset = 0;
+ }
+
+ pairSpan = new SnapshotSpan(startPoint, startPoint); // satisfy the compiler
+ return false;
+ }
+
+ private bool FindMatchingOpenChar(SnapshotPoint startPoint, char open, char close, int linesViewed, out SnapshotSpan pairSpan) {
+ ITextSnapshotLine line = startPoint.GetContainingLine();
+ int lineNumber = line.LineNumber;
+ int offset = startPoint.Position - line.Start.Position - 1; //move the offset to the character before this one
+
+ int lineNumberLimit = Math.Max(0, lineNumber - linesViewed);
+
+ int closeCount = 0;
+ while (true) {
+ string lineText = line.GetText();
+
+ //walk the entire line
+ for (; 0 <= offset; offset--) {
+ char currentChar = lineText[offset];
+ if (currentChar == open || currentChar == close) {
+ if (!InsideComment(new SnapshotPoint(line.Snapshot, line.Start.Position + offset))) {
+ if (currentChar == close) {
+ closeCount++;
+ } else if (0 < closeCount) {
+ closeCount--;
+ } else {
+ // We've found the open character
+ pairSpan = new SnapshotSpan(line.Start + offset, 1); //we just want the character itself
+ return true;
+ }
+ }
+ }
+ }
+
+ // Move to the previous line
+ lineNumber--;
+ if (lineNumber < lineNumberLimit)
+ break;
+
+ line = line.Snapshot.GetLineFromLineNumber(lineNumber);
+ offset = line.Length - 1;
+ }
+
+ pairSpan = new SnapshotSpan(startPoint, startPoint); // satisfy the compiler
+ return false;
+ }
+ }
+}
|