|
| 1 | +/*--------------------------------------------------------------------------------------------- |
| 2 | + * Copyright (c) Microsoft Corporation. All rights reserved. |
| 3 | + * Licensed under the MIT License. See License.txt in the project root for license information. |
| 4 | + *--------------------------------------------------------------------------------------------*/ |
| 5 | + |
| 6 | +import { ArrayQueue } from 'vs/base/common/arrays'; |
| 7 | +import { TextEditInfo } from 'vs/editor/common/model/bracketPairsTextModelPart/bracketPairsTree/beforeEditPositionMapper'; |
| 8 | +import { Length, lengthAdd, lengthDiffNonNegative, lengthEquals, lengthIsZero, lengthLessThanEqual, lengthZero, sumLengths } from 'vs/editor/common/model/bracketPairsTextModelPart/bracketPairsTree/length'; |
| 9 | + |
| 10 | +export function combineTextEditInfos(textEditInfoFirst: TextEditInfo[], textEditInfoSecond: TextEditInfo[]): TextEditInfo[] { |
| 11 | + if (textEditInfoFirst.length === 0) { |
| 12 | + return textEditInfoSecond; |
| 13 | + } |
| 14 | + |
| 15 | + // s0: State before any edits |
| 16 | + const firstMap = new ArrayQueue(toTextMap(textEditInfoFirst)); |
| 17 | + // s1: State after first edit, but before second edit |
| 18 | + const secondMap = toTextMap(textEditInfoSecond); |
| 19 | + // s2: State after both edits |
| 20 | + |
| 21 | + // If set, we are in an edit |
| 22 | + let remainingS0Length: Length | undefined = undefined; |
| 23 | + let remainingS1Length: Length = lengthZero; |
| 24 | + |
| 25 | + /** |
| 26 | + * @param s1Length Use undefined for length "infinity" |
| 27 | + */ |
| 28 | + function readPartialS0Map(s1Length: Length | undefined): TextMapping[] { |
| 29 | + const result: TextMapping[] = []; |
| 30 | + |
| 31 | + while (true) { |
| 32 | + if ((remainingS0Length !== undefined && !lengthIsZero(remainingS0Length)) || !lengthIsZero(remainingS1Length)) { |
| 33 | + let readS1Length: Length; |
| 34 | + if (s1Length !== undefined && lengthLessThanEqual(s1Length, remainingS1Length)) { |
| 35 | + // remaining satisfies request |
| 36 | + readS1Length = s1Length; |
| 37 | + remainingS1Length = lengthDiffNonNegative(s1Length, remainingS1Length); |
| 38 | + s1Length = lengthZero; |
| 39 | + } else { |
| 40 | + // Read all of remaining, potentially even more |
| 41 | + readS1Length = remainingS1Length; |
| 42 | + if (s1Length !== undefined) { |
| 43 | + s1Length = lengthDiffNonNegative(remainingS1Length, s1Length); |
| 44 | + } |
| 45 | + remainingS1Length = lengthZero; |
| 46 | + } |
| 47 | + |
| 48 | + if (remainingS0Length === undefined) { |
| 49 | + // unchanged area |
| 50 | + result.push({ |
| 51 | + oldLength: readS1Length, |
| 52 | + newLength: undefined |
| 53 | + }); |
| 54 | + } else { |
| 55 | + // We eagerly consume all of the old length, even if |
| 56 | + // we are in an edit and only consume it partially. |
| 57 | + result.push({ |
| 58 | + oldLength: remainingS0Length, |
| 59 | + newLength: readS1Length |
| 60 | + }); |
| 61 | + remainingS0Length = lengthZero; |
| 62 | + } |
| 63 | + } |
| 64 | + |
| 65 | + if (s1Length !== undefined && lengthIsZero(s1Length)) { |
| 66 | + break; |
| 67 | + } |
| 68 | + |
| 69 | + const item = firstMap.dequeue(); |
| 70 | + if (!item) { |
| 71 | + if (s1Length !== undefined) { |
| 72 | + result.push({ |
| 73 | + oldLength: s1Length, |
| 74 | + newLength: undefined, |
| 75 | + }); |
| 76 | + } |
| 77 | + break; |
| 78 | + } |
| 79 | + if (item.newLength === undefined) { |
| 80 | + remainingS1Length = item.oldLength; |
| 81 | + remainingS0Length = undefined; |
| 82 | + } else { |
| 83 | + remainingS0Length = item.oldLength; |
| 84 | + remainingS1Length = item.newLength; |
| 85 | + } |
| 86 | + } |
| 87 | + |
| 88 | + return result; |
| 89 | + } |
| 90 | + |
| 91 | + const result: TextEditInfo[] = []; |
| 92 | + |
| 93 | + function push(startOffset: Length, endOffset: Length, newLength: Length) { |
| 94 | + if (result.length > 0 && lengthEquals(result[result.length - 1].endOffset, startOffset)) { |
| 95 | + const lastResult = result[result.length - 1]; |
| 96 | + result[result.length - 1] = new TextEditInfo(lastResult.startOffset, endOffset, lengthAdd(lastResult.newLength, newLength)); |
| 97 | + } else { |
| 98 | + result.push({ startOffset, endOffset, newLength }); |
| 99 | + } |
| 100 | + } |
| 101 | + |
| 102 | + let s0offset = lengthZero; |
| 103 | + for (const s2 of secondMap) { |
| 104 | + const s0ToS1Map = readPartialS0Map(s2.oldLength); |
| 105 | + if (s2.newLength !== undefined) { |
| 106 | + // This is an edit |
| 107 | + const s0Length = sumLengths(s0ToS1Map, s => s.oldLength); |
| 108 | + const s0EndOffset = lengthAdd(s0offset, s0Length); |
| 109 | + push(s0offset, s0EndOffset, s2.newLength); |
| 110 | + s0offset = s0EndOffset; |
| 111 | + } else { |
| 112 | + // We are in an unchanged area |
| 113 | + for (const s1 of s0ToS1Map) { |
| 114 | + const s0startOffset = s0offset; |
| 115 | + s0offset = lengthAdd(s0offset, s1.oldLength); |
| 116 | + |
| 117 | + if (s1.newLength !== undefined) { |
| 118 | + push(s0startOffset, s0offset, s1.newLength); |
| 119 | + } |
| 120 | + } |
| 121 | + } |
| 122 | + } |
| 123 | + |
| 124 | + const s0ToS1Map = readPartialS0Map(undefined); |
| 125 | + for (const s1 of s0ToS1Map) { |
| 126 | + const s0startOffset = s0offset; |
| 127 | + s0offset = lengthAdd(s0offset, s1.oldLength); |
| 128 | + |
| 129 | + if (s1.newLength !== undefined) { |
| 130 | + push(s0startOffset, s0offset, s1.newLength); |
| 131 | + } |
| 132 | + } |
| 133 | + |
| 134 | + return result; |
| 135 | +} |
| 136 | + |
| 137 | +interface TextMapping { |
| 138 | + oldLength: Length; |
| 139 | + |
| 140 | + /** |
| 141 | + * If set, this mapping represents an edit. |
| 142 | + * If not set, this mapping represents an unchanged region (for which the new length equals the old length). |
| 143 | + */ |
| 144 | + newLength?: Length; |
| 145 | +} |
| 146 | + |
| 147 | +function toTextMap(textEditInfos: TextEditInfo[]): TextMapping[] { |
| 148 | + const result: TextMapping[] = []; |
| 149 | + let lastOffset = lengthZero; |
| 150 | + for (const textEditInfo of textEditInfos) { |
| 151 | + const spaceLength = lengthDiffNonNegative(lastOffset, textEditInfo.startOffset); |
| 152 | + if (!lengthIsZero(spaceLength)) { |
| 153 | + result.push({ oldLength: spaceLength }); |
| 154 | + } |
| 155 | + |
| 156 | + const oldLength = lengthDiffNonNegative(textEditInfo.startOffset, textEditInfo.endOffset); |
| 157 | + result.push({ oldLength, newLength: textEditInfo.newLength }); |
| 158 | + lastOffset = textEditInfo.endOffset; |
| 159 | + } |
| 160 | + return result; |
| 161 | +} |
0 commit comments