fix: remove cursor from users who move away from synced buffers

This commit is contained in:
zaaarf 2024-10-09 23:34:15 +02:00
parent 1e8306f6e4
commit 044b1f4470
No known key found for this signature in database
GPG key ID: C91CFF9E2262BBA1
3 changed files with 7 additions and 3 deletions

View file

@ -23,7 +23,7 @@ public class BufferSyncAction extends AnAction {
String[] active_buffers = CodeMP.getActiveWorkspace().activeBuffers(); String[] active_buffers = CodeMP.getActiveWorkspace().activeBuffers();
int choice = Messages.showChooseDialog( int choice = Messages.showChooseDialog(
"Detach from which buffer?", "Sync which buffer?",
"CodeMP Buffer Detach", "CodeMP Buffer Detach",
active_buffers, active_buffers,
"", "",

View file

@ -70,4 +70,4 @@ public class CursorEventListener implements CaretListener {
} }
})).start(); })).start();
} }
} }

View file

@ -49,7 +49,11 @@ public class CursorCallback implements Consumer<CursorController> {
try { try {
ApplicationManager.getApplication().runReadAction(() -> { ApplicationManager.getApplication().runReadAction(() -> {
Editor editor = FileUtil.getActiveEditorByPath(this.project, event.buffer); Editor editor = FileUtil.getActiveEditorByPath(this.project, event.buffer);
if(editor == null) return; if(editor == null) {
RangeHighlighter previous = CodeMP.HIGHLIGHTER_MAP.remove(event.user);
if(previous != null) previous.dispose();
return;
}
int startOffset = editor.getDocument().getLineStartOffset(event.startRow) + event.startCol; int startOffset = editor.getDocument().getLineStartOffset(event.startRow) + event.startCol;
int endOffset = editor.getDocument().getLineStartOffset(event.endRow) + event.endCol; int endOffset = editor.getDocument().getLineStartOffset(event.endRow) + event.endCol;