add prominent details button

Author: RemyDegenne

LeanExposition/Collect.lean

@@ -75,6 +75,7 @@ structure DeclCardData where
   isLemma : Bool := false
   isInstanceDecl : Bool := false
   tags : Array String := #[]
+  detailsUrl? : Option String := none
 deriving Repr, ToJson, FromJson, Inhabited
 
 /-- Data container for DetailsData. -/
@@ -314,10 +315,9 @@ def codeListParagraph (label : String) (items : Array String) : Option (Block Ma
       joinInlines entries #[.text " · "]
 
 /-- Helper for mkLinkParagraph. -/
-def mkLinkParagraph (sourceUrl? issueUrl? detailsUrl? : Option String) : Option (Block Manual) :=
+def mkLinkParagraph (sourceUrl? issueUrl? : Option String) : Option (Block Manual) :=
   let items :=
-    ([detailsUrl?.map fun url => .link #[.text "Details"] url,
-      sourceUrl?.map fun url => .link #[.text "Source"] url,
+    ([sourceUrl?.map fun url => .link #[.text "Source"] url,
       issueUrl?.map fun url => .link #[.text "Open Issue"] url].filterMap id)
   if items.isEmpty then
     none

LeanExposition/Site.lean

@@ -158,6 +158,11 @@ block_extension Block.declCard (_payload : DeclCardData) where
         .empty
       else
         {{<div class="decl-card-tags">{{tags}}</div>}}
+    let detailsHtml :=
+      if let some url := payload.detailsUrl? then
+        {{<a class="decl-card-action decl-card-details" href={{url}}>"Details"</a>}}
+      else
+        .empty
     let isMainTheorem := payload.kindLabel == "Theorem" && !payload.isLemma && !payload.isInstanceDecl
     let displayLabel :=
       if payload.isInstanceDecl then "Instance"
@@ -178,7 +183,7 @@ block_extension Block.declCard (_payload : DeclCardData) where
               <span class={{labelClass}}>{{displayLabel}}</span>
               <code class="decl-card-name">{{payload.fullName}}</code>
             </div>
-            <div class="decl-card-tagbar">{{tagsHtml}}</div>
+            <div class="decl-card-tagbar">{{detailsHtml}}{{tagsHtml}}</div>
           </div>
           <div class="decl-card-body">
             {{← contents.mapM goB}}
@@ -326,7 +331,7 @@ private def mkDeclBlock (decl : DeclInfo) (ctx : SiteContext) : Block Manual :=
       blocks := blocks.push <| .other (Block.details { summary := s!"Body uses ({proofDepLinks.size})" }) #[block]
     if let some block := depListBlock usedByLinks then
       blocks := blocks.push <| .other (Block.details { summary := s!"Used by ({usedByLinks.size})" }) #[block]
-    if let some block := mkLinkParagraph sourceUrl issueUrl detailsUrl then
+    if let some block := mkLinkParagraph sourceUrl issueUrl then
       blocks := blocks.push block
     if let some proof := decl.proofText? then
       blocks := blocks.push <| .other (Block.details { summary := "Proof" }) #[.code proof]
@@ -340,6 +345,7 @@ private def mkDeclBlock (decl : DeclInfo) (ctx : SiteContext) : Block Manual :=
       tags := #[
         if decl.dependsOnSorry then some "depends transitively on sorry" else none
       ].filterMap id
+      detailsUrl? := detailsUrl
     }
     .other (Block.declCard cardData) blocks
 

LeanExposition/Theme.lean

@@ -126,6 +126,8 @@ body {
 .decl-card-tagbar {
   align-items: flex-start;
   display: flex;
+  flex-wrap: wrap;
+  gap: 0.45rem;
   flex: 0 0 auto;
 }
 
@@ -139,6 +141,16 @@ body {
   text-decoration: none !important;
 }
 
+.decl-card-details {
+  background: var(--site-accent);
+  font-weight: 700;
+  box-shadow: 0 4px 12px rgba(214, 93, 93, 0.35);
+}
+
+.decl-card-details:hover {
+  background: var(--site-ink);
+}
+
 .decl-card details {
   border-top: 1px solid rgba(240, 212, 212, 0.9);
   margin-top: 0.9rem;