From 686f111438ec0dc2345799fc4110d5162f581303 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Wed, 15 Dec 2021 09:24:49 +0100 Subject: [PATCH] chore: Split Output.lean into multiple files --- DocGen4/Output.lean | 155 ++--------------------------------- DocGen4/Output/Base.lean | 47 +++++++++++ DocGen4/Output/Index.lean | 22 +++++ DocGen4/Output/Module.lean | 21 +++++ DocGen4/Output/Navbar.lean | 70 ++++++++++++++++ DocGen4/Output/NotFound.lean | 22 +++++ DocGen4/Output/Template.lean | 57 +++++++++++++ 7 files changed, 244 insertions(+), 150 deletions(-) create mode 100644 DocGen4/Output/Base.lean create mode 100644 DocGen4/Output/Index.lean create mode 100644 DocGen4/Output/Module.lean create mode 100644 DocGen4/Output/Navbar.lean create mode 100644 DocGen4/Output/NotFound.lean create mode 100644 DocGen4/Output/Template.lean diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index 91ac120..88ced36 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -4,160 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Henrik Böving -/ import Lean -import Std.Data.HashMap import DocGen4.Process -import DocGen4.ToHtmlFormat -import DocGen4.IncludeStr +import DocGen4.Output.Base +import DocGen4.Output.Index +import DocGen4.Output.Module +import DocGen4.Output.NotFound namespace DocGen4 -open Lean Std -open scoped DocGen4.Jsx -open IO System - -structure SiteContext where - root : String - result : AnalyzerResult - currentName : Option Name - -def setCurrentName (name : Name) (ctx : SiteContext) := {ctx with currentName := some name} - -abbrev HtmlM := Reader SiteContext - -def getRoot : HtmlM String := do (←read).root -def getResult : HtmlM AnalyzerResult := do (←read).result -def getCurrentName : HtmlM (Option Name) := do (←read).currentName - -def templateExtends {α β : Type} (base : α → HtmlM β) (new : HtmlM α) : HtmlM β := - new >>= base - -def nameToUrl (n : Name) : String := - (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html" - where - parts := n.components.map Name.toString - -def nameToDirectory (basePath : FilePath) (n : Name) : FilePath := - basePath / parts.foldl (λ acc p => acc / FilePath.mk p) (FilePath.mk ".") - where - parts := n.components.dropLast.map Name.toString - -def moduleListFile (file : Name) : HtmlM Html := do - let attributes := match ←getCurrentName with - | some name => - if file == name then - #[("class", "nav_link"), ("visible", "")] - else - #[("class", "nav_link")] - | none => #[("class", "nav_link")] - let nodes := #[{file.toString}] - return Html.element "div" attributes nodes - -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 dirNodes ← (dirs.mapM moduleListDir) - let fileNodes ← (files.mapM moduleListFile) - let attributes := match ←getCurrentName with - | some name => - if h.getName.isPrefixOf name then - #[("class", "nav_sect"), ("data-path", nameToUrl h.getName), ("open", "")] - else - #[("class", "nav_sect"), ("data-path", nameToUrl h.getName)] - | none => - #[("class", "nav_sect"), ("data-path", nameToUrl h.getName)] - let nodes := #[{h.getName.toString}] ++ dirNodes ++ fileNodes - return Html.element "details" attributes nodes - -def moduleList : HtmlM (Array Html) := do - let hierarchy := (←getResult).hierarchy - let mut list := Array.empty - for (n, cs) in hierarchy.getChildren do - list := list.push

{n.toString}

- list := list.push $ ←moduleListDir cs - list - -def navbar : HtmlM Html := do - - -def baseHtml (title : String) (site : Html) : HtmlM Html := do - - - - - - {title} - - - - - - - - -
-

Documentation

-

{title}

- -- TODO: Replace this form with our own search -
- - - -
-
- - - - {site} - - {←navbar} - - -- Lean in JS in HTML in Lean...very meta - - - -- TODO Add more js stuff - - - - -def notFound : HtmlM Html := do templateExtends (baseHtml "404") $ -
-

404 Not Found

-

Unfortunately, the page you were looking for is no longer here.

-
-
- -def index : HtmlM Html := do templateExtends (baseHtml "Index") $ -
- -

Welcome to the documentation page

- What is up? -
- -def styleCss : String := include_str "./static/style.css" -def navJs : String := include_str "./static/nav.js" - -def moduleToHtml (module : Module) : HtmlM Html := withReader (setCurrentName module.name) do - templateExtends (baseHtml module.name.toString) $ -
-

This is the page of {module.name.toString}

-
+open Lean Std IO System Output def htmlOutput (result : AnalyzerResult) : IO Unit := do -- TODO: parameterize this diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean new file mode 100644 index 0000000..5f18ab0 --- /dev/null +++ b/DocGen4/Output/Base.lean @@ -0,0 +1,47 @@ +/- +Copyright (c) 2021 Henrik Böving. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Henrik Böving +-/ +import Lean +import DocGen4.Process +import DocGen4.IncludeStr + +namespace DocGen4 +namespace Output + +open Lean System + +structure SiteContext where + root : String + result : AnalyzerResult + currentName : Option Name + +def setCurrentName (name : Name) (ctx : SiteContext) := {ctx with currentName := some name} + +abbrev HtmlM := Reader SiteContext + +def getRoot : HtmlM String := do (←read).root +def getResult : HtmlM AnalyzerResult := do (←read).result +def getCurrentName : HtmlM (Option Name) := do (←read).currentName + +def templateExtends {α β : Type} (base : α → HtmlM β) (new : HtmlM α) : HtmlM β := + new >>= base + +def nameToUrl (n : Name) : String := + (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html" + where + parts := n.components.map Name.toString + +def nameToDirectory (basePath : FilePath) (n : Name) : FilePath := + basePath / parts.foldl (· / ·) (FilePath.mk ".") + where + parts := n.components.dropLast.map Name.toString + +section Static + def styleCss : String := include_str "./static/style.css" + def navJs : String := include_str "./static/nav.js" +end Static + +end Output +end DocGen4 diff --git a/DocGen4/Output/Index.lean b/DocGen4/Output/Index.lean new file mode 100644 index 0000000..b09ac47 --- /dev/null +++ b/DocGen4/Output/Index.lean @@ -0,0 +1,22 @@ +/- +Copyright (c) 2021 Henrik Böving. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Henrik Böving +-/ +import DocGen4.ToHtmlFormat +import DocGen4.Output.Template + +namespace DocGen4 +namespace Output + +open scoped DocGen4.Jsx + +def index : HtmlM Html := do templateExtends (baseHtml "Index") $ +
+ +

Welcome to the documentation page

+ What is up? +
+ +end Output +end DocGen4 diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean new file mode 100644 index 0000000..44438b2 --- /dev/null +++ b/DocGen4/Output/Module.lean @@ -0,0 +1,21 @@ +/- +Copyright (c) 2021 Henrik Böving. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Henrik Böving +-/ +import DocGen4.ToHtmlFormat +import DocGen4.Output.Template + +namespace DocGen4 +namespace Output + +open scoped DocGen4.Jsx + +def moduleToHtml (module : Module) : HtmlM Html := withReader (setCurrentName module.name) do + templateExtends (baseHtml module.name.toString) $ +
+

This is the page of {module.name.toString}

+
+ +end Output +end DocGen4 diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean new file mode 100644 index 0000000..1975a70 --- /dev/null +++ b/DocGen4/Output/Navbar.lean @@ -0,0 +1,70 @@ +/- +Copyright (c) 2021 Henrik Böving. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Henrik Böving +-/ +import Lean +import DocGen4.ToHtmlFormat +import DocGen4.Output.Base + +namespace DocGen4 +namespace Output + +open Lean +open scoped DocGen4.Jsx + +def moduleListFile (file : Name) : HtmlM Html := do + let attributes := match ←getCurrentName with + | some name => + if file == name then + #[("class", "nav_link"), ("visible", "")] + else + #[("class", "nav_link")] + | none => #[("class", "nav_link")] + let nodes := #[{file.toString}] + return Html.element "div" attributes nodes + +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 dirNodes ← (dirs.mapM moduleListDir) + let fileNodes ← (files.mapM moduleListFile) + let attributes := match ←getCurrentName with + | some name => + if h.getName.isPrefixOf name then + #[("class", "nav_sect"), ("data-path", nameToUrl h.getName), ("open", "")] + else + #[("class", "nav_sect"), ("data-path", nameToUrl h.getName)] + | none => + #[("class", "nav_sect"), ("data-path", nameToUrl h.getName)] + let nodes := #[{h.getName.toString}] ++ dirNodes ++ fileNodes + return Html.element "details" attributes nodes + +def moduleList : HtmlM (Array Html) := do + let hierarchy := (←getResult).hierarchy + let mut list := Array.empty + for (n, cs) in hierarchy.getChildren do + list := list.push

{n.toString}

+ list := list.push $ ←moduleListDir cs + list + +def navbar : HtmlM Html := do + + +end Output +end DocGen4 diff --git a/DocGen4/Output/NotFound.lean b/DocGen4/Output/NotFound.lean new file mode 100644 index 0000000..ed5d547 --- /dev/null +++ b/DocGen4/Output/NotFound.lean @@ -0,0 +1,22 @@ +/- +Copyright (c) 2021 Henrik Böving. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Henrik Böving +-/ +import DocGen4.ToHtmlFormat +import DocGen4.Output.Template + +namespace DocGen4 +namespace Output + +open scoped DocGen4.Jsx + +def notFound : HtmlM Html := do templateExtends (baseHtml "404") $ +
+

404 Not Found

+

Unfortunately, the page you were looking for is no longer here.

+
+
+ +end Output +end DocGen4 diff --git a/DocGen4/Output/Template.lean b/DocGen4/Output/Template.lean new file mode 100644 index 0000000..5d82257 --- /dev/null +++ b/DocGen4/Output/Template.lean @@ -0,0 +1,57 @@ +/- +Copyright (c) 2021 Henrik Böving. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Henrik Böving +-/ +import DocGen4.ToHtmlFormat +import DocGen4.Output.Navbar + +namespace DocGen4 +namespace Output + +open scoped DocGen4.Jsx + +def baseHtml (title : String) (site : Html) : HtmlM Html := do + + + + + + {title} + + + + + + + + +
+

Documentation

+

{title}

+ -- TODO: Replace this form with our own search +
+ + + +
+
+ + + + {site} + + {←navbar} + + -- Lean in JS in HTML in Lean...very meta + + + -- TODO Add more js stuff + + + + +end Output +end DocGen4