feat: mobile reading (#148)

Update Verso to get CSS fixes for mobile browsers, and make the preview banner less ostentatious.
leanprover · Nov 15, 2024 · a725f98 · a725f98
1 parent 6d7aca6
commit a725f98
Show file tree

Hide file tree

Showing 3 changed files with 30 additions and 26 deletions.
diff --git a/Manual/Meta/Marginalia.lean b/Manual/Meta/Marginalia.lean
@@ -22,30 +22,41 @@ def Marginalia.css := r#"
   padding: 0.5rem;
 }
 /* Wide viewport */
-@media (min-width: 1400px) {
-.marginalia .note {
-  float: right;
-  clear: right;
-  margin-right: -19vw;
-  width: 15vw;
-  margin-top: 1rem;
-}
+@media screen and (min-width: 1400px) {
+  .marginalia .note {
+    float: right;
+    clear: right;
+    margin-right: -19vw;
+    width: 15vw;
+    margin-top: 1rem;
+  }
 }
 
 .marginalia:hover, .marginalia:hover .note, .marginalia:has(.note:hover) {
   background-color: var(--lean-accent-light-blue);
 }
 
-/* Narrow viewport */
-@media (max-width: 1400px) {
-.marginalia .note {
-  float: right;
-  clear: right;
-  width: 40%;
-  margin: 1rem 0;
-  margin-left: 5%;
+/* Medium viewport */
+@media screen and (700px < width <= 1400px) {
+  .marginalia .note {
+    float: right;
+    clear: right;
+    width: 40%;
+    margin: 1rem 0;
+    margin-left: 5%;
+  }
 }
+
+/* Narrow viewport (e.g. phone) */
+@media screen and (width <= 700px) {
+  .marginalia .note {
+    float: left;
+    clear: left;
+    width: 90%;
+    margin: 1rem 5%;
+  }
 }
+
 body {
   counter-reset: margin-note-counter;
 }

diff --git a/lake-manifest.json b/lake-manifest.json
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "b1d1865f979882dbc52c386877bc6708d9b56aec",
+   "rev": "314e77088df5c4fa8e072d88e66af3599aca8350",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

diff --git a/static/theme.css b/static/theme.css
@@ -115,18 +115,11 @@ figcaption {
         position: fixed;
         top: 0;
         right: 0;
-        transform:
-            /* first undo the effect of the rotation, pushing it to the right*/
-            translateX(25%)
-            /* then shove it against the side, sticking the box out of the viewport */
-            translateX(5em) translateY(-5em)
-            /* and rotate! */
-            rotate(45deg);
-        transform-origin: top left;
-        padding: 1em 8em;
+        padding: 0.5rem 1rem;
         background-color: var(--lean-compl-yellow);
         font-family: var(--verso-structure-font-family);
         font-size: large;
+        z-index: 9; /* Just below the ToC */
     }
 }