#257: size the paste gutter to the widest line number

The paste gutter was pinned to a fixed 3ch width. With box-sizing:
border-box that leaves only ~19px of content after the 10px+10px side
padding, so 2+ digit line numbers overflow right into the code text
(owner-visible from line 10, worst at 100+).

paste-lines.js now sets the gutter width to calc(Nch + 20px), where N is
the digit count of the highest line number, via CSSOM (CSP forbids
inline style attributes). Numbers were already right-aligned; the column
now matches the width of the biggest number. The width is only written
when it changes, so the resize-observer/renumber loop keeps a stable
fixed point.

internal/web/static/paste-lines.js

@@ -44,6 +44,23 @@
   // measured, not derived from span counts or heights.
   function renumber() {
     var lines = body.querySelectorAll('.codeline');
+    // #257: size the gutter column to the widest line number so numbers in
+    // the 100s+ fit their own column instead of bleeding into the code text.
+    // The gutter is box-sizing: border-box, so the column width must be the
+    // digits PLUS the 10px left + 10px right padding; at the CSS default 3ch
+    // the padding alone leaves only ~19px of content, and any 2+ digit
+    // number overflows into the code. Numbers are right-aligned, and the
+    // width below fits the widest number exactly. Set via CSSOM (CSP
+    // forbids inline style attributes). Only touch the width when it
+    // changes: the resize observer below re-runs renumber() when the gutter
+    // width reflows the code column, and rewriting the same value would
+    // ping-pong the fixed point forever.
+    var digits = String(lines.length || 1).length;
+    var w = 'calc(' + digits + 'ch + 20px)';
+    if (gutter.style.width !== w) {
+      gutter.style.minWidth = w;
+      gutter.style.width = w;
+    }
     if (!wrapOn() || !lines.length) {
       // wrap OFF: one number per logical line (pre-existing behavior,
       // including the gutter scrolling with horizontal scroll).