feat: Revamp the hierarchy mechanism

Previously the hierarchy mechanism wouldn't show modules in files that
have names, equal to some directory with submodules.
main
Henrik Böving 2021-12-13 20:47:52 +01:00
parent 9256aaa0fc
commit d2594669fa
2 changed files with 39 additions and 29 deletions

View File

@ -21,9 +21,9 @@ def getNLevels (name : Name) (levels: Nat) : Name :=
components := name.components'
inductive Hierarchy where
| node : Name → RBNode Name (λ _ => Hierarchy) → Hierarchy
| node (name : Name) (isFile : Bool) (children : RBNode Name (λ _ => Hierarchy)) : Hierarchy
instance : Inhabited Hierarchy := ⟨Hierarchy.node Name.anonymous RBNode.leaf⟩
instance : Inhabited Hierarchy := ⟨Hierarchy.node Name.anonymous false RBNode.leaf⟩
abbrev HierarchyMap := RBNode Name (λ _ => Hierarchy)
@ -43,35 +43,45 @@ end HierarchyMap
namespace Hierarchy
def empty (n : Name) : Hierarchy := node n RBNode.leaf
def empty (n : Name) (isFile : Bool) : Hierarchy :=
node n isFile RBNode.leaf
def getName : Hierarchy → Name
| node n _ => n
| node n _ _ => n
def getChildren : Hierarchy → HierarchyMap
| node _ c => c
| node _ _ c => c
def isFile : Hierarchy → Bool
| node _ f _ => f
partial def insert! (h : Hierarchy) (n : Name) : Hierarchy := Id.run $ do
let hn := h.getName
let mut cs := h.getChildren
if getDepth hn ≥ getDepth n then
panic! "Invalid insert"
else if getDepth hn + 1 == getDepth n then
assert! getDepth hn ≤ getDepth n
if getDepth hn + 1 == getDepth n then
match cs.find Name.cmp n with
| none =>
node hn (cs.insert Name.cmp n $ empty n)
| some _ => h
node hn h.isFile (cs.insert Name.cmp n $ empty n true)
| some (node _ true _) => h
| some hierarchy@(node _ false ccs) =>
cs := cs.erase Name.cmp n
node hn h.isFile (cs.insert Name.cmp n $ node n true ccs)
else
let leveledName := getNLevels n (getDepth hn + 1)
match cs.find Name.cmp leveledName with
| some nextLevel =>
cs := cs.erase Name.cmp leveledName
node hn $ cs.insert Name.cmp leveledName (nextLevel.insert! n)
-- BUG?
node hn h.isFile $ cs.insert Name.cmp leveledName (nextLevel.insert! n)
| none =>
let child := (insert! (empty leveledName) n)
node hn $ cs.insert Name.cmp leveledName child
let child := (insert! (empty leveledName false) n)
node hn h.isFile $ cs.insert Name.cmp leveledName child
partial def fromArray (names : Array Name) : Hierarchy := names.foldl insert! (empty anonymous)
partial def fromArray (names : Array Name) : Hierarchy :=
names.foldl insert! (empty anonymous false)
end Hierarchy
end DocGen4

View File

@ -37,19 +37,19 @@ def nameToDirectory (basePath : FilePath) (n : Name) : FilePath :=
where
parts := n.components.dropLast.map Name.toString
partial def moduleListAux (h : Hierarchy) : HtmlM Html := do
if h.getChildren.toList.length == 0 then
<div «class»="nav_link visible">
<a href={s!"{←getRoot}{nameToUrl h.getName}"}>{h.getName.toString}</a>
def moduleListFile (file : Name) : HtmlM Html := do
<div «class»="nav_link">
<a href={s!"{←getRoot}{nameToUrl file}"}>{file.toString}</a>
</div>
else
partial def moduleListDir (h : Hierarchy) : HtmlM Html := do
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 <details «class»="nav_sect" «data-path»={←nameToUrl h.getName}>
let dirs := children.filter (λ c => c.getChildren.toList.length != 0)
let files := children.filter Hierarchy.isFile |>.map Hierarchy.getName
return <details «class»="nav_sect" «data-path»={nameToUrl h.getName}>
<summary>{h.getName.toString}</summary>
[nodes]
[(←(dirs.mapM moduleListDir))]
[(←(files.mapM moduleListFile))]
</details>
def moduleList : HtmlM (Array Html) := do
@ -57,7 +57,7 @@ def moduleList : HtmlM (Array Html) := do
let mut list := Array.empty
for (n, cs) in hierarchy.getChildren do
list := list.push <h4>{n.toString}</h4>
list := list.push $ ←moduleListAux cs
list := list.push $ ←moduleListDir cs
list
def navbar : HtmlM Html := do