sync header width in opened editors

edit/header-resizer.js

@@ -4,12 +4,16 @@
 'use strict';
 
 (function HeaderResizer() {
+  const PREF_ID = 'editor.headerWidth';
   const el = $('#header-resizer');
   let lastW, lastX;
-
+  prefs.subscribe(PREF_ID, (key, val) => {
+    setLastWidth();
+    setWidth(val);
+  });
   el.onmousedown = e => {
     if (e.button) return;
-    lastW = $('#header').clientWidth;
+    setLastWidth();
     lastX = e.clientX;
     document.body.classList.add('resizing-h');
     document.on('mousemove', resize);
@@ -17,15 +21,11 @@
   };
 
   function resize({clientX: x}) {
-    const w = editor.updateHeaderWidth(lastW + x - lastX);
+    const w = setWidth(lastW + x - lastX);
-    const delta = w - lastW;
+    if (!w) return;
-    if (!delta) return;
     lastW = w;
     lastX = x;
-    prefs.set('editor.headerWidth', w);
+    prefs.set(PREF_ID, w);
-    for (const el of $$('.CodeMirror-linewidget[style*="width:"]')) {
-      el.style.width = parseFloat(el.style.width) - delta + 'px';
-    }
   }
 
   function resizeStop() {
@@ -33,4 +33,18 @@
     document.off('mousemove', resize);
     document.body.classList.remove('resizing-h');
   }
+
+  function setLastWidth() {
+    lastW = $('#header').clientWidth;
+  }
+
+  /** @returns {number|void} new width in case it's different, otherwise void */
+  function setWidth(w) {
+    const delta = (w = editor.updateHeaderWidth(w)) - lastW;
+    if (!delta) return;
+    for (const el of $$('.CodeMirror-linewidget[style*="width:"]')) {
+      el.style.width = parseFloat(el.style.width) - delta + 'px';
+    }
+    return w;
+  }
 })();