Add a zoom control

index.html

@@ -100,6 +100,10 @@
             <path d="M5,6 a1,1 0 0,0 2,0 a1,1 0 1,1 1,1 a1,1 0 0,0 -1,1 v1 a1,1 0 1,0 2,0 v-0.17 A3,3 0 1,0 5,6"></path>
             <circle cx="8" cy="12" r="1"></circle>
         </g>
+        <g id="svg-icon-zoom">
+            <path d="M1,6 a5,5 0 1,1 10,0 a5,5 0 1,1 -10,0 m2,0 a3,3 0 1,0 6,0 a3,3 0 1,0 -6,0"></path>
+            <path d="M14,12 l-2,2 -4,-4 2,-2 4,4"></path>
+        </g>
     </defs>
     </svg>
     <header id="header-main">

js/main-editor.js

@@ -3254,9 +3254,33 @@ export class Editor extends PrimaryView {
 
         // Populate status bar (needs doing before the mouse stuff, which tries to update it)
         let statusbar = this.root.querySelector('#editor-statusbar');
-        this.statusbar_zoom = mk('div.-zoom');
+        this.statusbar_zoom = mk('output');
+        this.statusbar_zoom_input = mk('input', {type: 'range', min: 0, max: EDITOR_ZOOM_LEVELS.length - 1});
+        this.statusbar_zoom_input.addEventListener('input', ev => {
+            let index = parseInt(ev.target.value, 10);
+            if (index < 0) {
+                index = 0;
+            }
+            else if (index >= EDITOR_ZOOM_LEVELS.length) {
+                index = EDITOR_ZOOM_LEVELS.length - 1;
+            }
+            // Center the zoom on the center of the viewport
+            let rect = this.actual_viewport_el.getBoundingClientRect();
+            this.set_canvas_zoom(
+                EDITOR_ZOOM_LEVELS[index],
+                (rect.left + rect.right) / 2,
+                (rect.top + rect.bottom) / 2);
+        });
         this.statusbar_cursor = mk('div.-mouse', "—");
-        statusbar.append(this.statusbar_zoom, this.statusbar_cursor);
+        statusbar.append(
+            mk('div.-zoom',
+                mk_svg('svg.svg-icon', {viewBox: '0 0 16 16'},
+                    mk_svg('use', {href: `#svg-icon-zoom`})),
+                this.statusbar_zoom_input,
+                this.statusbar_zoom,
+            ),
+            this.statusbar_cursor,
+        );
 
         // Keyboard shortcuts
         window.addEventListener('keydown', ev => {
@@ -4202,6 +4226,12 @@ export class Editor extends PrimaryView {
         this.actual_viewport_el.classList.toggle('--crispy', this.zoom >= 1);
         this.statusbar_zoom.textContent = `${this.zoom * 100}%`;
 
+        let index = EDITOR_ZOOM_LEVELS.findIndex(el => el >= this.zoom);
+        if (index < 0) {
+            index = EDITOR_ZOOM_LEVELS.length - 1;
+        }
+        this.statusbar_zoom_input.value = index;
+
         // Only actually adjust the scroll position after changing the zoom, or it might not be
         // possible to scroll that far yet
         if (scroll_adjust_x !== null) {

style.css

@@ -2012,6 +2012,7 @@ body.--debug #player-debug {
 #editor #editor-statusbar {
     grid-area: status;
     display: flex;
+    align-items: center;
     gap: 0.5em;
     /* Try very hard to minimize reflow, since this is updated frequently */
     height: 1.25em;
@@ -2019,6 +2020,16 @@ body.--debug #player-debug {
     overflow: hidden;
 }
 #editor #editor-statusbar > .-zoom {
+    display: flex;
+    align-items: center;
+    gap: 0.25em;
+    width: 11.5em;
+}
+#editor #editor-statusbar > .-zoom > input {
+    width: 6em;
+    margin: 0;
+}
+#editor #editor-statusbar > .-zoom > output {
     width: 4em;
 }
 #editor #editor-statusbar > .-cursor {