From 02271ed8d12f2d33efeed3a0eb6b8a45b810f3ee Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@davidchristiansen.dk>
Date: Mon, 9 Dec 2024 11:36:20 +0100
Subject: [PATCH] fix: docstring structure inheritance filters

---
 src/verso-manual/VersoManual/Docstring.lean | 24 ++++++++++++++-------
 1 file changed, 16 insertions(+), 8 deletions(-)

diff --git a/src/verso-manual/VersoManual/Docstring.lean b/src/verso-manual/VersoManual/Docstring.lean
index 5c84f1e..09b2469 100644
--- a/src/verso-manual/VersoManual/Docstring.lean
+++ b/src/verso-manual/VersoManual/Docstring.lean
@@ -460,18 +460,21 @@ def docstringStyle := r#"
   margin: 0;
   padding: 0;
 }
+
 .namedocs .extends li {
   list-style-type: none;
   display: inline-block;
-  padding-right: 1rem;
 }
 
-.namedocs:has(input[data-parent-idx="0"]) tr[data-inherited-from="0"] {
-  display: none;
+.namedocs .extends li label {
+  padding-right: 1rem;
 }
 
-.namedocs:has(input[data-parent-idx="0"]:checked) tr[data-inherited-from="0"] {
-  display: table-row;
+.namedocs:has(input[data-parent-idx]) tr[data-inherited-from] {
+  transition-property: opacity, display;
+  transition-duration: 0.4s;
+  transition-behavior: allow-discrete;
+  @starting-style { opacity: 0 !important; }
 }
 "# ++ Id.run do
   let mut str := ""
@@ -482,11 +485,16 @@ where
   mkFilterRule (i : Nat) : String :=
     ".namedocs:has(input[data-parent-idx=\"" ++ toString i ++ "\"]) tr[data-inherited-from=\"" ++ toString i ++ "\"] {
   display: none;
+  opacity: 0;
 }
 .namedocs:has(input[data-parent-idx=\"" ++ toString i ++ "\"]:checked) tr[data-inherited-from=\"" ++ toString i ++"\"] {
   display: table-row;
+  transform: none;
+  opacity: 1;
+}
+.namedocs:has(input[data-parent-idx=\"" ++ toString i ++ "\"]:checked):has(tr.inheritance[data-inherited-from=\"" ++ toString i ++"\"] .parent:hover) tr[data-inherited-from]:not([data-inherited-from=\"" ++ toString i ++"\"]) {
+  opacity: 0.5;
 }
-
 "
 
 
@@ -621,9 +629,9 @@ where
               if i.fieldFrom.isEmpty then pure Html.empty
               else
                   pure {{
-                    <tr class="inheritance" {{inheritedAttr}}>
+                    <tr class=s!"inheritance from{inheritedAttrVal.getD "_"}" {{inheritedAttr}}>
                       <td colspan="2"></td>
-                      <td>
+                      <td class="parent">
                         "Inherited from "
                         <ol>
                         {{ ← i.fieldFrom.mapM fun p => do