mirror of
https://github.com/hexedtech/codemp-vscode.git
synced 2024-11-22 07:24:49 +01:00
fix: last changes to resync
This commit is contained in:
parent
45f52535da
commit
87f2b6f2fb
1 changed files with 5 additions and 5 deletions
|
@ -36,7 +36,7 @@ export async function apply_changes_to_buffer(path: string, controller: codemp.B
|
||||||
.replace(range, event.content)
|
.replace(range, event.content)
|
||||||
})) {
|
})) {
|
||||||
vscode.window.showWarningMessage("Couldn't apply changes");
|
vscode.window.showWarningMessage("Couldn't apply changes");
|
||||||
await resync(path, workspace, editor, 20);
|
await resync(path, workspace, editor, 100);
|
||||||
}
|
}
|
||||||
locks.delete(path);
|
locks.delete(path);
|
||||||
|
|
||||||
|
@ -116,7 +116,7 @@ export async function attach_to_remote_buffer(buffer_name: string, set_content?:
|
||||||
editor.document.positionAt(0),
|
editor.document.positionAt(0),
|
||||||
editor.document.positionAt(doc_len)
|
editor.document.positionAt(doc_len)
|
||||||
);
|
);
|
||||||
locks.set(buffer_name, `${0}..${doc_len}:${remoteContent}`);
|
locks.set(buffer_name, remoteContent);
|
||||||
await editor.edit(editBuilder => {
|
await editor.edit(editBuilder => {
|
||||||
editBuilder
|
editBuilder
|
||||||
.replace(range, remoteContent)
|
.replace(range, remoteContent)
|
||||||
|
@ -125,10 +125,10 @@ export async function attach_to_remote_buffer(buffer_name: string, set_content?:
|
||||||
}
|
}
|
||||||
|
|
||||||
let disposable = vscode.workspace.onDidChangeTextDocument(async (event: vscode.TextDocumentChangeEvent) => {
|
let disposable = vscode.workspace.onDidChangeTextDocument(async (event: vscode.TextDocumentChangeEvent) => {
|
||||||
if (!mapping.bufferMapper.by_editor(event.document.uri)) return;
|
if (file_uri != event.document.uri) return;
|
||||||
let skip_this = locks.get(buffer_name);
|
let skip_this = locks.get(buffer_name);
|
||||||
for (let change of event.contentChanges) {
|
for (let change of event.contentChanges) {
|
||||||
if (skip_this && change.text == skip_this) continue;
|
if (skip_this !== undefined && change.text == skip_this) continue;
|
||||||
// LOGGER.info(`onDidChangeTextDocument(event: [${change.rangeOffset}, ${change.text}, ${change.rangeOffset + change.rangeLength}])`);
|
// LOGGER.info(`onDidChangeTextDocument(event: [${change.rangeOffset}, ${change.text}, ${change.rangeOffset + change.rangeLength}])`);
|
||||||
await buffer.send({
|
await buffer.send({
|
||||||
start: change.rangeOffset,
|
start: change.rangeOffset,
|
||||||
|
@ -241,7 +241,7 @@ export async function resync(buffer_name: string, workspace: codemp.Workspace, e
|
||||||
locks.set(buffer_name, content);
|
locks.set(buffer_name, content);
|
||||||
for (let i = 0; i < tries; i++) {
|
for (let i = 0; i < tries; i++) {
|
||||||
if (await editor.edit(editBuilder => editBuilder.replace(range, content))) {
|
if (await editor.edit(editBuilder => editBuilder.replace(range, content))) {
|
||||||
console.log("attempts to sync", tries);
|
console.log("attempts to sync", i);
|
||||||
break;
|
break;
|
||||||
}
|
}
|
||||||
if (i == tries-1) {
|
if (i == tries-1) {
|
||||||
|
|
Loading…
Reference in a new issue