Skip to content

Commit

Permalink
fix: docstring structure inheritance filters
Browse files Browse the repository at this point in the history
  • Loading branch information
david-christiansen committed Dec 9, 2024
1 parent cc3a037 commit 02271ed
Showing 1 changed file with 16 additions and 8 deletions.
24 changes: 16 additions & 8 deletions src/verso-manual/VersoManual/Docstring.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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 := ""
Expand All @@ -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;
}
"


Expand Down Expand Up @@ -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
Expand Down

0 comments on commit 02271ed

Please sign in to comment.