diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index a11618f..4d92118 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -13,6 +13,7 @@ namespace DocGen4 open Lean Std open scoped DocGen4.Jsx +open IO System structure SiteContext where root : String @@ -26,22 +27,27 @@ def getResult : HtmlM AnalyzerResult := do (←read).result def templateExtends {α β : Type} (base : α → HtmlM β) (new : HtmlM α) : HtmlM β := new >>= base -def nameToPath (n : Name) : String := +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 + partial def moduleListAux (h : Hierarchy) : HtmlM Html := do if h.getChildren.toList.length == 0 then
else let children := Array.mk (h.getChildren.toList.map Prod.snd) -- TODO: Is having no children really the correct criterium for a clickable module? let (dirs, files) := children.partition (λ c => c.getChildren.toList.length != 0) let nodes := (←(dirs.mapM moduleListAux)) ++ (←(files.mapM moduleListAux)) - return