diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean
index 88ced36..ce81d2f 100644
--- a/DocGen4/Output.lean
+++ b/DocGen4/Output.lean
@@ -27,8 +27,8 @@ def htmlOutput (result : AnalyzerResult) : IO Unit := do
FS.writeFile (basePath / "nav.js") navJs
for (module, content) in result.modules.toArray do
let moduleHtml := ReaderT.run (moduleToHtml content) config
- let path := basePath / (nameToUrl module)
- FS.createDirAll $ nameToDirectory basePath module
+ let path := moduleNameToFile basePath module
+ FS.createDirAll $ moduleNameToDirectory basePath module
FS.writeFile path moduleHtml.toString
end DocGen4
diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean
index 5f18ab0..2e4b07a 100644
--- a/DocGen4/Output/Base.lean
+++ b/DocGen4/Output/Base.lean
@@ -28,12 +28,18 @@ def getCurrentName : HtmlM (Option Name) := do (←read).currentName
def templateExtends {α β : Type} (base : α → HtmlM β) (new : HtmlM α) : HtmlM β :=
new >>= base
-def nameToUrl (n : Name) : String :=
+-- TODO: Change this to HtmlM and auto add the root URl
+def moduleNameToUrl (n : Name) : String :=
(parts.intersperse "/").foldl (· ++ ·) "" ++ ".html"
where
parts := n.components.map Name.toString
-def nameToDirectory (basePath : FilePath) (n : Name) : FilePath :=
+def moduleNameToFile (basePath : FilePath) (n : Name) : FilePath :=
+ FilePath.withExtension (basePath / parts.foldl (· / ·) (FilePath.mk ".")) "html"
+ where
+ parts := n.components.map Name.toString
+
+def moduleNameToDirectory (basePath : FilePath) (n : Name) : FilePath :=
basePath / parts.foldl (· / ·) (FilePath.mk ".")
where
parts := n.components.dropLast.map Name.toString
diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean
index 1975a70..27da4c0 100644
--- a/DocGen4/Output/Navbar.lean
+++ b/DocGen4/Output/Navbar.lean
@@ -21,7 +21,7 @@ def moduleListFile (file : Name) : HtmlM Html := do
else
#[("class", "nav_link")]
| none => #[("class", "nav_link")]
- let nodes := #[{file.toString}]
+ let nodes := #[{file.toString}]
return Html.element "div" attributes nodes
partial def moduleListDir (h : Hierarchy) : HtmlM Html := do
@@ -33,11 +33,11 @@ partial def moduleListDir (h : Hierarchy) : HtmlM Html := do
let attributes := match ←getCurrentName with
| some name =>
if h.getName.isPrefixOf name then
- #[("class", "nav_sect"), ("data-path", nameToUrl h.getName), ("open", "")]
+ #[("class", "nav_sect"), ("data-path", moduleNameToUrl h.getName), ("open", "")]
else
- #[("class", "nav_sect"), ("data-path", nameToUrl h.getName)]
+ #[("class", "nav_sect"), ("data-path", moduleNameToUrl h.getName)]
| none =>
- #[("class", "nav_sect"), ("data-path", nameToUrl h.getName)]
+ #[("class", "nav_sect"), ("data-path", moduleNameToUrl h.getName)]
let nodes := #[{h.getName.toString}] ++ dirNodes ++ fileNodes
return Html.element "details" attributes nodes