feat: make logo on manual into link to root

leanprover · Dec 16, 2024 · 3bca47a · 3bca47a
1 parent 10bba0b
commit 3bca47a
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 1 deletion.
diff --git a/src/verso-manual/VersoManual/Html.lean b/src/verso-manual/VersoManual/Html.lean
@@ -467,6 +467,7 @@ def page
     (showNavButtons : Bool := true)
     (base : Option String := none)
     (logo : Option String := none)
+    (logoLink : Option String := none)
     (repoLink : Option String := none)
     (issueLink : Option String := none)
     (extraStylesheets : List String := [])
@@ -500,7 +501,13 @@ def page
           <nav id="toc">
             <input type="checkbox" id="toggle-toc" checked="checked"/>
             <div class="first">
-              {{if let some url := logo then {{<img src={{url}} id="logo"/>}} else .empty }}
+              {{if let some url := logo then
+                  let logoHtml := {{<img src={{url}}/>}}
+                  let logoDest :=
+                    if let some root := logoLink then root
+                    else relativeRoot
+                  {{<a href={{logoDest}} id="logo">{{logoHtml}}</a>}}
+                else .empty }}
               {{if showNavButtons then toc.navButtons path else .empty}}
               {{toc.localHtml path}}
             </div>

diff --git a/src/verso-manual/VersoManual/Html/Style.lean b/src/verso-manual/VersoManual/Html/Style.lean
@@ -374,6 +374,14 @@ pre, code {
   transition: height var(--verso-toc-transition-time) ease-in-out;
 }
 
+#logo img {
+  object-fit: contain;
+  max-width: 100%;
+  max-height: 4rem;
+  margin-left: auto;
+  display: block;
+}
+
 /******** Headerline ********/
 
 #toggle-toc-click {