Better scaling of images in HTML output

Turn on the previously disabled automatic scaling of images in HTML
output.  To avoid images looking too large on nowadays-normal screens,
restrict the width to 75% on such screens.

Some work is still necessary because SVG images without a viewBox
still won't scale, but that will a separate patch.

Discussion: https://www.postgresql.org/message-id/flat/6d2442d1-84a2-36ef-e014-b6d1ece8a139%40postgresql.org

diff --git a/doc/src/sgml/stylesheet-html-common.xsl b/doc/src/sgml/stylesheet-html-common.xsl
index b105005235d7824faac1185e140fee9520c9334a..9edce52a104476eeb65c850cba6a57c0d7c1018e 100644 (file)
--- a/doc/src/sgml/stylesheet-html-common.xsl
+++ b/doc/src/sgml/stylesheet-html-common.xsl
@@ -14,7 +14,7 @@
 
 
 
-ignore.image.scaling" select="1"/>
+make.graphic.viewport" select="0"/>
 [email protected]
 2
 

diff --git a/doc/src/sgml/stylesheet.css b/doc/src/sgml/stylesheet.css
index c355fbecac74d6fb4ee8d915e0778e07d18c109d..1a66c789d50b1260a91d58f8ab5a975ddd71efc5 100644 (file)
--- a/doc/src/sgml/stylesheet.css
+++ b/doc/src/sgml/stylesheet.css
@@ -102,3 +102,10 @@ var        { font-family: monospace; font-style: italic; }
 acronym        { font-style: inherit; }
 
 .option        { white-space: nowrap; }
+
+/* make images not too wide on larger screens */
+@media (min-width: 800px) {
+  .mediaobject {
+    width: 75%;
+  }
+}