From 828449ebb429ea3934affcf37c6c703036d16a57 Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Fri, 18 Feb 2022 14:03:54 +0800 Subject: [PATCH 1/4] fix: add nav link to non leaf node modules --- DocGen4/Output/Navbar.lean | 2 +- DocGen4/ToHtmlFormat.lean | 8 ++++---- static/style.css | 7 ++----- 3 files changed, 7 insertions(+), 10 deletions(-) diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean index d2d4792..008ebdf 100644 --- a/DocGen4/Output/Navbar.lean +++ b/DocGen4/Output/Navbar.lean @@ -28,7 +28,7 @@ partial def moduleListDir (h : Hierarchy) : HtmlM Html := do pure
- {h.getName.toString} + {h.getName.toString} [dirNodes] [fileNodes]
diff --git a/DocGen4/ToHtmlFormat.lean b/DocGen4/ToHtmlFormat.lean index beddf74..c4226d5 100644 --- a/DocGen4/ToHtmlFormat.lean +++ b/DocGen4/ToHtmlFormat.lean @@ -33,9 +33,9 @@ def attributesToString (attrs : Array (String × String)) :String := -- TODO: Termination proof partial def toStringAux : Html → String -| element tag false attrs #[text s] => s!"<{tag}{attributesToString attrs}>{s}\n" -| element tag false attrs #[child] => s!"<{tag}{attributesToString attrs}>\n{child.toStringAux}\n" -| element tag false attrs children => s!"<{tag}{attributesToString attrs}>\n{children.foldl (· ++ toStringAux ·) ""}\n" +| element tag false attrs #[text s] => s!"<{tag}{attributesToString attrs}>{s}" +| element tag false attrs #[child] => s!"<{tag}{attributesToString attrs}>{child.toStringAux}" +| element tag false attrs children => s!"<{tag}{attributesToString attrs}>{children.foldl (· ++ toStringAux ·) ""}" | element tag true attrs children => s!"<{tag}{attributesToString attrs}>{children.foldl (· ++ toStringAux ·) ""}" | text s => s @@ -107,7 +107,7 @@ macro_rules let mut cs ← `(#[]) for child in children do 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` | `(jsxChild|{$t}) => `(($cs).push ($t : Html)) | `(jsxChild|[$t]) => `($cs ++ ($t : Array Html)) diff --git a/static/style.css b/static/style.css index 7e28a65..a4e0c9a 100644 --- a/static/style.css +++ b/static/style.css @@ -273,13 +273,10 @@ nav { margin-top: 1ex; } -.nav details > * { +.nav details, .nav_link { padding-left: 2ex; } -.nav summary { - cursor: pointer; - padding-left: 0; -} + .nav summary::marker { font-size: 85%; } From 2f5a95b312498453753348c4404df2f8e25cb134 Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Fri, 18 Feb 2022 14:03:54 +0800 Subject: [PATCH 2/4] fix: add nav link to non leaf node modules --- DocGen4/Output/Navbar.lean | 2 +- DocGen4/ToHtmlFormat.lean | 6 +++--- static/style.css | 7 ++----- 3 files changed, 6 insertions(+), 9 deletions(-) diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean index d2d4792..008ebdf 100644 --- a/DocGen4/Output/Navbar.lean +++ b/DocGen4/Output/Navbar.lean @@ -28,7 +28,7 @@ partial def moduleListDir (h : Hierarchy) : HtmlM Html := do pure
- {h.getName.toString} + {h.getName.toString} [dirNodes] [fileNodes]
diff --git a/DocGen4/ToHtmlFormat.lean b/DocGen4/ToHtmlFormat.lean index beddf74..d96f2a9 100644 --- a/DocGen4/ToHtmlFormat.lean +++ b/DocGen4/ToHtmlFormat.lean @@ -33,9 +33,9 @@ def attributesToString (attrs : Array (String × String)) :String := -- TODO: Termination proof partial def toStringAux : Html → String -| element tag false attrs #[text s] => s!"<{tag}{attributesToString attrs}>{s}\n" -| element tag false attrs #[child] => s!"<{tag}{attributesToString attrs}>\n{child.toStringAux}\n" -| element tag false attrs children => s!"<{tag}{attributesToString attrs}>\n{children.foldl (· ++ toStringAux ·) ""}\n" +| element tag false attrs #[text s] => s!"<{tag}{attributesToString attrs}>{s}" +| element tag false attrs #[child] => s!"<{tag}{attributesToString attrs}>{child.toStringAux}" +| element tag false attrs children => s!"<{tag}{attributesToString attrs}>{children.foldl (· ++ toStringAux ·) ""}" | element tag true attrs children => s!"<{tag}{attributesToString attrs}>{children.foldl (· ++ toStringAux ·) ""}" | text s => s diff --git a/static/style.css b/static/style.css index 7e28a65..a4e0c9a 100644 --- a/static/style.css +++ b/static/style.css @@ -273,13 +273,10 @@ nav { margin-top: 1ex; } -.nav details > * { +.nav details, .nav_link { padding-left: 2ex; } -.nav summary { - cursor: pointer; - padding-left: 0; -} + .nav summary::marker { font-size: 85%; } From c31aef8e87b3e7e78aa7a5001ea0308f66f244c8 Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Sat, 19 Feb 2022 01:54:20 +0800 Subject: [PATCH 3/4] fix: remove redundant link to parent module --- DocGen4/Output/Navbar.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean index 008ebdf..1b8a530 100644 --- a/DocGen4/Output/Navbar.lean +++ b/DocGen4/Output/Navbar.lean @@ -21,7 +21,8 @@ def moduleListFile (file : Name) : HtmlM Html := do partial def moduleListDir (h : Hierarchy) : HtmlM Html := do let children := Array.mk (h.getChildren.toList.map Prod.snd) let dirs := children.filter (λ c => c.getChildren.toList.length != 0) - let files := children.filter Hierarchy.isFile |>.map Hierarchy.getName + let files := children.filter (λ c => Hierarchy.isFile c ∧ c.getChildren.toList.length = 0) + |>.map Hierarchy.getName let dirNodes ← (dirs.mapM moduleListDir) let fileNodes ← (files.mapM moduleListFile) let moduleLink ← moduleNameToLink h.getName From 1ef736c014e9e98d7b2c0d932a5b35128821e6de Mon Sep 17 00:00:00 2001 From: Xubai Wang Date: Sat, 19 Feb 2022 02:07:25 +0800 Subject: [PATCH 4/4] fix: use flattened Html element --- DocGen4/Output/Navbar.lean | 2 +- DocGen4/ToHtmlFormat.lean | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean index 1b8a530..efc9735 100644 --- a/DocGen4/Output/Navbar.lean +++ b/DocGen4/Output/Navbar.lean @@ -29,7 +29,7 @@ partial def moduleListDir (h : Hierarchy) : HtmlM Html := do pure
- {h.getName.toString} + {Html.element "summary" true #[] #[{h.getName.toString}]} [dirNodes] [fileNodes]
diff --git a/DocGen4/ToHtmlFormat.lean b/DocGen4/ToHtmlFormat.lean index d96f2a9..beddf74 100644 --- a/DocGen4/ToHtmlFormat.lean +++ b/DocGen4/ToHtmlFormat.lean @@ -33,9 +33,9 @@ def attributesToString (attrs : Array (String × String)) :String := -- TODO: Termination proof partial def toStringAux : Html → String -| element tag false attrs #[text s] => s!"<{tag}{attributesToString attrs}>{s}" -| element tag false attrs #[child] => s!"<{tag}{attributesToString attrs}>{child.toStringAux}" -| element tag false attrs children => s!"<{tag}{attributesToString attrs}>{children.foldl (· ++ toStringAux ·) ""}" +| element tag false attrs #[text s] => s!"<{tag}{attributesToString attrs}>{s}\n" +| element tag false attrs #[child] => s!"<{tag}{attributesToString attrs}>\n{child.toStringAux}\n" +| element tag false attrs children => s!"<{tag}{attributesToString attrs}>\n{children.foldl (· ++ toStringAux ·) ""}\n" | element tag true attrs children => s!"<{tag}{attributesToString attrs}>{children.foldl (· ++ toStringAux ·) ""}" | text s => s