feat: auto-refresh FileNav on write_file, replace_file_content, and run_command

Backend emits terminal events for write_file, replace_file_content,
and run_command. Frontend showFileNavDir subscriber uses startsWith
path matching to smartly refresh only when the event is relevant:
- write_file/replace_file_content: refresh if path is in current view
- run_command: always refresh (uses root '/' which matches everything)
- Also adds copy-to-clipboard button and code preview full-height fix
This commit is contained in:
Timothy Jaeryang Baek
2026-03-05 14:41:18 -06:00
parent 3b97c8d89b
commit 828656b35f
3 changed files with 32 additions and 15 deletions
+5 -2
View File
@@ -406,11 +406,14 @@
};
const terminalEventHandler = (type: string, data: any) => {
if (!data?.path) return;
if (type === 'terminal:display_file') {
if (!data?.path) return;
displayFileHandler(data.path, { showControls, showFileNavPath });
} else if (type === 'terminal:write_file') {
} else if (type === 'terminal:write_file' || type === 'terminal:replace_file_content') {
if (!data?.path) return;
showFileNavDir.set(data.path);
} else if (type === 'terminal:run_command') {
showFileNavDir.set('/');
}
};
+11 -7
View File
@@ -511,13 +511,15 @@
const lastSlash = filePath.lastIndexOf('/');
const dir = lastSlash > 0 ? filePath.substring(0, lastSlash + 1) : '/';
if (dir === currentPath) {
await loadDir(currentPath);
}
if (filePath === selectedFile) {
const fileName = filePath.substring(lastSlash + 1);
const entry = entries.find((e) => e.name === fileName);
if (entry) await openEntry(entry);
if (selectedFile) {
if (selectedFile === filePath || currentPath.startsWith(dir)) {
const fileName = selectedFile.split('/').pop() ?? '';
await openEntry({ name: fileName, type: 'file', size: 0 });
}
} else {
if (currentPath.startsWith(dir) || dir.startsWith(currentPath)) {
await loadDir(currentPath);
}
}
});
@@ -549,6 +551,8 @@
document.addEventListener('visibilitychange', onVisibilityChange);
return () => {
unsubFileNav();
unsubFileNavDir();
window.removeEventListener('keydown', onKeyDown);
window.removeEventListener('keyup', onKeyUp);
window.removeEventListener('blur', onBlur);