From 3bca47aded57a0aa9fe253c3db1542f1bf9300d9 Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@davidchristiansen.dk>
Date: Mon, 16 Dec 2024 13:50:27 +0100
Subject: [PATCH] feat: make logo on manual into link to root

---
 src/verso-manual/VersoManual/Html.lean       | 9 ++++++++-
 src/verso-manual/VersoManual/Html/Style.lean | 8 ++++++++
 2 files changed, 16 insertions(+), 1 deletion(-)

diff --git a/src/verso-manual/VersoManual/Html.lean b/src/verso-manual/VersoManual/Html.lean
index 78ace5f..d260998 100644
--- 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
index 72dfaf7..b1dbdec 100644
--- 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 {