js: Take device pixel ratio into account when setting default size

This is a bit of a hack.  When setting the puzzle to its default size,
either at startup or from a right-click on the resize handle, we now
scale the default size from midend_size() by the device pixel ratio,
and then pass that back to midend_size().  This does more or less the
right thing, in that the puzzle now starts up at a size that scales
with the font size.

There are still some slight inconsistencies, where sequences of DPR
changes and puzzle parameter changes can have order-dependent effects
on the size of the puzzle.  Happily these effects are small and fairly
hard to observe.

emcclib.js

@@ -569,6 +569,15 @@ mergeInto(LibraryManager.library, {
         nominal_height = onscreen_canvas.height / dpr;
     },
 
+    /*
+     * double js_get_device_pixel_ratio();
+     *
+     * Return the current device pixel ratio.
+     */
+    js_get_device_pixel_ratio: function() {
+        return window.devicePixelRatio || 1;
+    },
+
     /*
      * void js_dialog_init(const char *title);
      *