fix: add nav link to non leaf node modules
parent
2dac93d360
commit
828449ebb4
|
@ -28,7 +28,7 @@ partial def moduleListDir (h : Hierarchy) : HtmlM Html := do
|
||||||
pure
|
pure
|
||||||
<details "class"="nav_sect" "data-path"={moduleLink}
|
<details "class"="nav_sect" "data-path"={moduleLink}
|
||||||
[if (←getCurrentName).any (h.getName.isPrefixOf ·) then #[("open", "")] else #[]]>
|
[if (←getCurrentName).any (h.getName.isPrefixOf ·) then #[("open", "")] else #[]]>
|
||||||
<summary>{h.getName.toString}</summary>
|
<summary><a "href"={← moduleNameToLink h.getName}>{h.getName.toString}</a></summary>
|
||||||
[dirNodes]
|
[dirNodes]
|
||||||
[fileNodes]
|
[fileNodes]
|
||||||
</details>
|
</details>
|
||||||
|
|
|
@ -33,9 +33,9 @@ def attributesToString (attrs : Array (String × String)) :String :=
|
||||||
|
|
||||||
-- TODO: Termination proof
|
-- TODO: Termination proof
|
||||||
partial def toStringAux : Html → String
|
partial def toStringAux : Html → String
|
||||||
| element tag false attrs #[text s] => s!"<{tag}{attributesToString attrs}>{s}</{tag}>\n"
|
| element tag false attrs #[text s] => s!"<{tag}{attributesToString attrs}>{s}</{tag}>"
|
||||||
| element tag false attrs #[child] => s!"<{tag}{attributesToString attrs}>\n{child.toStringAux}</{tag}>\n"
|
| element tag false attrs #[child] => s!"<{tag}{attributesToString attrs}>{child.toStringAux}</{tag}>"
|
||||||
| element tag false attrs children => s!"<{tag}{attributesToString attrs}>\n{children.foldl (· ++ toStringAux ·) ""}</{tag}>\n"
|
| element tag false attrs children => s!"<{tag}{attributesToString attrs}>{children.foldl (· ++ toStringAux ·) ""}</{tag}>"
|
||||||
| element tag true attrs children => s!"<{tag}{attributesToString attrs}>{children.foldl (· ++ toStringAux ·) ""}</{tag}>"
|
| element tag true attrs children => s!"<{tag}{attributesToString attrs}>{children.foldl (· ++ toStringAux ·) ""}</{tag}>"
|
||||||
| text s => s
|
| text s => s
|
||||||
|
|
||||||
|
@ -107,7 +107,7 @@ macro_rules
|
||||||
let mut cs ← `(#[])
|
let mut cs ← `(#[])
|
||||||
for child in children do
|
for child in children do
|
||||||
cs ← match child with
|
cs ← match child with
|
||||||
| `(jsxChild|$t:jsxText) => `(($cs).push (Html.text $(quote t[0].getAtomVal!)))
|
| `(jsxChild|$t:jsxText) => `(($cs).push (Html.text $(quote t[0].getAtomVal!))
|
||||||
-- TODO(WN): elab as list of children if type is `t Html` where `Foldable t`
|
-- TODO(WN): elab as list of children if type is `t Html` where `Foldable t`
|
||||||
| `(jsxChild|{$t}) => `(($cs).push ($t : Html))
|
| `(jsxChild|{$t}) => `(($cs).push ($t : Html))
|
||||||
| `(jsxChild|[$t]) => `($cs ++ ($t : Array Html))
|
| `(jsxChild|[$t]) => `($cs ++ ($t : Array Html))
|
||||||
|
|
|
@ -273,13 +273,10 @@ nav {
|
||||||
margin-top: 1ex;
|
margin-top: 1ex;
|
||||||
}
|
}
|
||||||
|
|
||||||
.nav details > * {
|
.nav details, .nav_link {
|
||||||
padding-left: 2ex;
|
padding-left: 2ex;
|
||||||
}
|
}
|
||||||
.nav summary {
|
|
||||||
cursor: pointer;
|
|
||||||
padding-left: 0;
|
|
||||||
}
|
|
||||||
.nav summary::marker {
|
.nav summary::marker {
|
||||||
font-size: 85%;
|
font-size: 85%;
|
||||||
}
|
}
|
||||||
|
|
Loading…
Reference in New Issue