266
continue;
267
}
269
>
// make sure diff won't take too long
270
>
if (Math.max(text.length, original.length) > EditorWorker._diffLimit) {
271
result.push({ range, text });
272
continue;
273
}
275
>
// compute diff between original and edit.text
276
>
const changes = stringDiff(original, text, pretty);
277
>
const editOffset = model.offsetAt(Range.lift(range).getStartPosition());
278
>
279
>
for (const change of changes) {
280
>
const start = model.positionAt(editOffset + change.originalStart);
281
>
const end = model.positionAt(editOffset + change.originalStart + change.originalLength);
282
>
const newEdit: TextEdit = {
283
>
text: text.substr(change.modifiedStart, change.modifiedLength),
284
>
range: { startLineNumber: start.lineNumber, startColumn: start.column, endLineNumber: end.lineNumber, endColumn: end.column }
285
>
};
286
>
287
>
if (model.getValueInRange(newEdit.range) !== newEdit.text) {
288
>
result.push(newEdit);
289
>
}
290
>
}
291
>
}
292
293
if (typeof lastEol === 'number') {