dashboard: keep selections

1 files changed, 29 insertions, 3 deletions

diff --git a/src/api/dashboard/dashboard.html b/src/api/dashboard/dashboard.html
index 4f77dde..d5642a9 100644
--- a/src/api/dashboard/dashboard.html
+++ b/src/api/dashboard/dashboard.html
@@ -654,7 +654,15 @@ function documentEntry(key, summary, path) {
   return details;
 }
 // The node says what changed (paths), or that anything may have (`all`).
+// Changes waiting while the document box is busy (`busy`): merged, applied after.
+let documentPending = null;
 function documentChanged(change) {
+  if (busy(document.getElementById("document-box"))) {
+    documentPending = documentPending === null ? change
+      : documentPending.all || change.all ? { all: true }
+      : { paths: [...documentPending.paths, ...change.paths] };
+    return;
+  }
   for (const [id, branch] of documentBranches) {
     if (!branch.element.isConnected) { documentBranches.delete(id); continue; }
     if (change.all || change.paths.some(path => related(path, branch.path))) branch.refresh();
@@ -663,14 +671,32 @@ function documentChanged(change) {
 document.getElementById("document").replaceChildren(
   documentEntry("store", { type: "map", size: "…" }, []));
 
+// A box is busy while text in it is selected: drawing it anew would lose the selection,
+// so it waits (`held`) until the selection is gone.
+function busy(box) {
+  const selection = window.getSelection();
+  if (!selection || selection.isCollapsed || !selection.rangeCount) return false;
+  return box.contains(selection.getRangeAt(0).commonAncestorContainer);
+}
+let held = false;
 function render() {
   if (!state) return;
   document.getElementById("node").textContent =
     (state.node.alias ? state.node.alias + " · " : "") + state.node.id;
-  renderPeers();
-  renderStats();
-  renderGraph();
+  held = false;
+  for (const [box, draw] of [["peers-box", renderPeers], ["figures-box", renderStats],
+    ["map", renderGraph]]) {
+    if (busy(document.getElementById(box))) held = true; else draw();
+  }
 }
+document.addEventListener("selectionchange", () => {
+  if (held) render();
+  if (documentPending !== null && !busy(document.getElementById("document-box"))) {
+    const change = documentPending;
+    documentPending = null;
+    documentChanged(change);
+  }
+});
 
 // A click beside the nodes: back to this node.
 const graph = document.getElementById("graph");