| 94 | } |
| 95 | |
| 96 | function writeTabToUrl(name, { push = true } = {}) { |
| 97 | try { |
| 98 | const url = new URL(window.location); |
| 99 | if (url.searchParams.get("tab") === name) return; |
| 100 | url.searchParams.set("tab", name); |
| 101 | if (push) window.history.pushState({ tab: name }, "", url); |
| 102 | else window.history.replaceState({ tab: name }, "", url); |
| 103 | } catch { |
| 104 | /* URL state is best-effort */ |
| 105 | } |
| 106 | } |
| 107 | |
| 108 | // --------------------------------------------------------------------------- |
| 109 | // Error boundary — wraps each plugin tab so one crash can't blank the shell |