feat: resync if hash mismatch

This commit is contained in:
zaaarf 2024-09-26 14:56:47 +02:00
parent 249a01d841
commit db89c781a6
No known key found for this signature in database
GPG key ID: C91CFF9E2262BBA1
2 changed files with 14 additions and 8 deletions

View file

@ -1,5 +1,5 @@
[versions] [versions]
codemp = '0.7.0' codemp = '0.7.2'
lombok = '1.18.34' lombok = '1.18.34'
intellij-plugin = '2.0.1' intellij-plugin = '2.0.1'
git-version = '3.1.0' git-version = '3.1.0'

View file

@ -6,6 +6,7 @@ import com.intellij.openapi.editor.Editor;
import com.intellij.openapi.project.Project; import com.intellij.openapi.project.Project;
import lombok.RequiredArgsConstructor; import lombok.RequiredArgsConstructor;
import mp.code.BufferController; import mp.code.BufferController;
import mp.code.Extensions;
import mp.code.data.TextChange; import mp.code.data.TextChange;
import mp.code.exceptions.ControllerException; import mp.code.exceptions.ControllerException;
import mp.code.intellij.CodeMP; import mp.code.intellij.CodeMP;
@ -46,18 +47,23 @@ public class BufferCallback implements Consumer<BufferController> {
changeList.add(change); changeList.add(change);
} }
ApplicationManager.getApplication().runWriteAction(() -> ApplicationManager.getApplication().runWriteAction(() -> {
CommandProcessor.getInstance().executeCommand( CommandProcessor.getInstance().executeCommand(
this.project, this.project,
() -> changeList.forEach((change) -> () -> changeList.forEach((change) -> {
editor.getDocument().replaceString( editor.getDocument().replaceString((int) change.start, (int) change.end, change.content);
(int) change.start, (int) change.end, change.content) // check for validity, force-sync if mismatch
), if(change.hash.isPresent() && change.hash.getAsLong() != Extensions.hash(editor.getDocument().getText())) {
try {
editor.getDocument().setText(bufferController.getContent());
} catch(ControllerException ignored) {} // ignore exception
}
}),
"CodeMPBufferReceive", "CodeMPBufferReceive",
"codemp-buffer-receive", "codemp-buffer-receive",
editor.getDocument() editor.getDocument()
) );
); });
}); });
}); });
}); });