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") $
-
-
-
-
+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