From ea10ba265550e54a002dce378c678d5f1365f865 Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@davidchristiansen.dk>
Date: Fri, 15 Nov 2024 22:17:26 +0100
Subject: [PATCH] fix: marginal notes now work better on narrow phone screens

---
 Manual/Meta/Marginalia.lean | 43 +++++++++++++++++++++++--------------
 1 file changed, 27 insertions(+), 16 deletions(-)

diff --git a/Manual/Meta/Marginalia.lean b/Manual/Meta/Marginalia.lean
index 7a6197c..84881f5 100644
--- 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;
 }