js: Pay attention to changes in device pixel ratio

Because it's the simplest thing to do, when we notice such a change we
keep the current puzzle at its existing size measured in device
pixels.  This has the rather odd consequence that when changing the
text size in Firefox, the size of the puzzle remains constant.

emccpre.js

@@ -526,6 +526,19 @@ function initPuzzle() {
         }
     });
 
+    /*
+     * Arrange to detect changes of device pixel ratio.  Adapted from
+     * <https://developer.mozilla.org/en-US/docs/Web/API/Window/
+     * devicePixelRatio> (CC0).
+     */
+    const update_pixel_ratio = () => {
+        let dpr = window.devicePixelRatio;
+        resizable_div.style.width = onscreen_canvas.width / dpr + "px";
+        matchMedia(`(resolution: ${dpr}dppx)`)
+            .addEventListener("change", update_pixel_ratio, { once: true })
+    }
+    update_pixel_ratio();
+
     Module.onRuntimeInitialized = function() {
         // Run the C setup function, passing argv[1] as the fragment
         // identifier (so that permalinks of the form puzzle.html#game-id