/-
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.Output.ToHtmlFormat
import DocGen4.Output.Base
namespace DocGen4
namespace Output
open Lean
open scoped DocGen4.Jsx
def moduleListFile (file : NameExt) : BaseHtmlM Html := do
let contents :=
if file.ext == .pdf then
{s!"π {file.getString!} (pdf)"}
else
{file.getString!}
return
{contents}
/--
Build the HTML tree representing the module hierarchy.
-/
partial def moduleListDir (h : Hierarchy) : BaseHtmlM Html := do
let children := Array.mk (h.getChildren.toList.map Prod.snd)
let nodes β children.mapM (fun c =>
if c.getChildren.toList.length != 0 then
moduleListDir c
else if Hierarchy.isFile c && c.getChildren.toList.length = 0 then
moduleListFile (Hierarchy.getNameExt c)
else
pure ""
)
let moduleLink β moduleNameToLink h.getName
let summary :=
if h.isFile then
{s!"{h.getName.getString!} ({file})"}
else
{h.getName.getString!}
pure
{summary}
[nodes]
/--
Return a list of top level modules, linkified and rendered as HTML
-/
def moduleList : BaseHtmlM Html := do
let hierarchy β getHierarchy
let mut list := Array.empty
for (_, cs) in hierarchy.getChildren do
list := list.push <| β moduleListDir cs
return
[list]
/--
The main entry point to rendering the navbar on the left hand side.
-/
def navbar : BaseHtmlM Html := do
pure
[β baseHtmlHeadDeclarations]