diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean
index e6c4074..6d7593f 100644
--- a/DocGen4/Output/Base.lean
+++ b/DocGen4/Output/Base.lean
@@ -97,6 +97,7 @@ def templateExtends {α β} {m} [Bind m] (base : α → m β) (new : m α) : m
def templateLiftExtends {α β} {m n} [Bind m] [MonadLift n m] (base : α → n β) (new : m α) : m β :=
new >>= (monadLift ∘ base)
+
/--
Returns the doc-gen4 link to a module name.
-/
@@ -104,6 +105,13 @@ def moduleNameToLink (n : Name) : BaseHtmlM String := do
let parts := n.components.map Name.toString
return (← getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html"
+/-
+Returns the doc-gen4 link to a module `NameExt`.
+-/
+def moduleNameExtToLink (n : NameExt) : BaseHtmlM String := do
+ let parts := n.name.components.map Name.toString
+ return (← getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ "." ++ n.ext.toString
+
/--
Returns the HTML doc-gen4 link to a module name.
-/
diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean
index 33f06f7..dd7ad7e 100644
--- a/DocGen4/Output/Navbar.lean
+++ b/DocGen4/Output/Navbar.lean
@@ -13,9 +13,14 @@ namespace Output
open Lean
open scoped DocGen4.Jsx
-def moduleListFile (file : Name) : BaseHtmlM Html := do
- return
-
{file.getString!}
+def moduleListFile (file : NameExt) : BaseHtmlM Html := do
+ let contents :=
+ if file.ext == .pdf then
+
{s!"🗎 {file.getString!} (pdf)"}
+ else
+
{file.getString!}
+ return
+ {contents}
/--
@@ -23,11 +28,14 @@ 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 dirs := children.filter (fun c => c.getChildren.toList.length != 0)
- let files := children.filter (fun c => Hierarchy.isFile c && c.getChildren.toList.length = 0)
- |>.map Hierarchy.getName
- let dirNodes ← dirs.mapM moduleListDir
- let fileNodes ← files.mapM moduleListFile
+ 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
@@ -38,8 +46,7 @@ partial def moduleListDir (h : Hierarchy) : BaseHtmlM Html := do
pure
{summary}
- [dirNodes]
- [fileNodes]
+ [nodes]
/--
diff --git a/DocGen4/Process.lean b/DocGen4/Process.lean
index 0c1d9e6..dd6a317 100644
--- a/DocGen4/Process.lean
+++ b/DocGen4/Process.lean
@@ -14,6 +14,7 @@ import DocGen4.Process.DocInfo
import DocGen4.Process.Hierarchy
import DocGen4.Process.InductiveInfo
import DocGen4.Process.InstanceInfo
+import DocGen4.Process.NameExt
import DocGen4.Process.NameInfo
import DocGen4.Process.OpaqueInfo
import DocGen4.Process.StructureInfo
diff --git a/DocGen4/Process/Hierarchy.lean b/DocGen4/Process/Hierarchy.lean
index 9502078..3d1b703 100644
--- a/DocGen4/Process/Hierarchy.lean
+++ b/DocGen4/Process/Hierarchy.lean
@@ -6,6 +6,8 @@ Authors: Henrik Böving
import Lean
import Lean.Data.HashMap
+import DocGen4.Process.NameExt
+
def Lean.HashSet.fromArray [BEq α] [Hashable α] (xs : Array α) : Lean.HashSet α :=
xs.foldr (flip .insert) .empty
@@ -18,35 +20,38 @@ def getNLevels (name : Name) (levels: Nat) : Name :=
(components.drop (components.length - levels)).reverse.foldl (· ++ ·) Name.anonymous
inductive Hierarchy where
-| node (name : Name) (isFile : Bool) (children : RBNode Name (fun _ => Hierarchy)) : Hierarchy
+| node (name : NameExt) (isFile : Bool) (children : RBNode NameExt (fun _ => Hierarchy)) : Hierarchy
-instance : Inhabited Hierarchy := ⟨Hierarchy.node Name.anonymous false RBNode.leaf⟩
+instance : Inhabited Hierarchy := ⟨Hierarchy.node ⟨anonymous, .html⟩ false RBNode.leaf⟩
-abbrev HierarchyMap := RBNode Name (fun _ => Hierarchy)
+abbrev HierarchyMap := RBNode NameExt (fun _ => Hierarchy)
-- Everything in this namespace is adapted from stdlib's RBNode
namespace HierarchyMap
-def toList : HierarchyMap → List (Name × Hierarchy)
+def toList : HierarchyMap → List (NameExt × Hierarchy)
| t => t.revFold (fun ps k v => (k, v)::ps) []
-def toArray : HierarchyMap → Array (Name × Hierarchy)
+def toArray : HierarchyMap → Array (NameExt × Hierarchy)
| t => t.fold (fun ps k v => ps ++ #[(k, v)] ) #[]
-def hForIn [Monad m] (t : HierarchyMap) (init : σ) (f : (Name × Hierarchy) → σ → m (ForInStep σ)) : m σ :=
+def hForIn [Monad m] (t : HierarchyMap) (init : σ) (f : (NameExt × Hierarchy) → σ → m (ForInStep σ)) : m σ :=
t.forIn init (fun a b acc => f (a, b) acc)
-instance : ForIn m HierarchyMap (Name × Hierarchy) where
+instance : ForIn m HierarchyMap (NameExt × Hierarchy) where
forIn := HierarchyMap.hForIn
end HierarchyMap
namespace Hierarchy
-def empty (n : Name) (isFile : Bool) : Hierarchy :=
+def empty (n : NameExt) (isFile : Bool) : Hierarchy :=
node n isFile RBNode.leaf
def getName : Hierarchy → Name
+| node n _ _ => n.name
+
+def getNameExt : Hierarchy → NameExt
| node n _ _ => n
def getChildren : Hierarchy → HierarchyMap
@@ -55,31 +60,34 @@ def getChildren : Hierarchy → HierarchyMap
def isFile : Hierarchy → Bool
| node _ f _ => f
-partial def insert! (h : Hierarchy) (n : Name) : Hierarchy := Id.run do
- let hn := h.getName
+partial def insert! (h : Hierarchy) (n : NameExt) : Hierarchy := Id.run do
+ let hn := h.getNameExt
let mut cs := h.getChildren
- if getNumParts hn + 1 == getNumParts n then
- match cs.find Name.cmp n with
+ if getNumParts hn.name + 1 == getNumParts n.name then
+ match cs.find NameExt.cmp n with
| none =>
- node hn h.isFile (cs.insert Name.cmp n <| empty n true)
+ node hn h.isFile (cs.insert NameExt.cmp n <| empty n true)
| some (node _ true _) => h
| some (node _ false ccs) =>
- cs := cs.erase Name.cmp n
- node hn h.isFile (cs.insert Name.cmp n <| node n true ccs)
+ cs := cs.erase NameExt.cmp n
+ node hn h.isFile (cs.insert NameExt.cmp n <| node n true ccs)
else
- let leveledName := getNLevels n (getNumParts hn + 1)
- match cs.find Name.cmp leveledName with
+ let leveledName := ⟨getNLevels n.name (getNumParts hn.name + 1), .html⟩
+ match cs.find NameExt.cmp leveledName with
| some nextLevel =>
- cs := cs.erase Name.cmp leveledName
+ cs := cs.erase NameExt.cmp leveledName
-- BUG?
- node hn h.isFile <| cs.insert Name.cmp leveledName (nextLevel.insert! n)
+ node hn h.isFile <| cs.insert NameExt.cmp leveledName (nextLevel.insert! n)
| none =>
let child := (insert! (empty leveledName false) n)
- node hn h.isFile <| cs.insert Name.cmp leveledName child
+ node hn h.isFile <| cs.insert NameExt.cmp leveledName child
partial def fromArray (names : Array Name) : Hierarchy :=
- names.foldl insert! (empty anonymous false)
+ (names.map (fun n => NameExt.mk n .html)).foldl insert! (empty ⟨anonymous, .html⟩ false)
+
+partial def fromArrayExt (names : Array NameExt) : Hierarchy :=
+ names.foldl insert! (empty ⟨anonymous, .html⟩ false)
def baseDirBlackList : HashSet String :=
HashSet.fromArray #[
@@ -102,13 +110,15 @@ def baseDirBlackList : HashSet String :=
"style.css"
]
-partial def fromDirectoryAux (dir : System.FilePath) (previous : Name) : IO (Array Name) := do
+partial def fromDirectoryAux (dir : System.FilePath) (previous : Name) : IO (Array NameExt) := do
let mut children := #[]
for entry in ← System.FilePath.readDir dir do
if ← entry.path.isDir then
children := children ++ (← fromDirectoryAux entry.path (.str previous entry.fileName))
else if entry.path.extension = some "html" then
- children := children.push <| .str previous (entry.fileName.dropRight ".html".length)
+ children := children.push <| ⟨.str previous (entry.fileName.dropRight ".html".length), .html⟩
+ else if entry.path.extension = some "pdf" then
+ children := children.push <| ⟨.str previous (entry.fileName.dropRight ".pdf".length), .pdf⟩
return children
def fromDirectory (dir : System.FilePath) : IO Hierarchy := do
@@ -119,8 +129,10 @@ def fromDirectory (dir : System.FilePath) : IO Hierarchy := do
else if ← entry.path.isDir then
children := children ++ (← fromDirectoryAux entry.path (.mkSimple entry.fileName))
else if entry.path.extension = some "html" then
- children := children.push <| .mkSimple (entry.fileName.dropRight ".html".length)
- return Hierarchy.fromArray children
+ children := children.push <| ⟨.mkSimple (entry.fileName.dropRight ".html".length), .html⟩
+ else if entry.path.extension = some "pdf" then
+ children := children.push <| ⟨.mkSimple (entry.fileName.dropRight ".pdf".length), .pdf⟩
+ return Hierarchy.fromArrayExt children
end Hierarchy
end DocGen4
diff --git a/DocGen4/Process/NameExt.lean b/DocGen4/Process/NameExt.lean
new file mode 100644
index 0000000..d1be339
--- /dev/null
+++ b/DocGen4/Process/NameExt.lean
@@ -0,0 +1,48 @@
+/-
+A generalization of `Lean.Name` that includes a file extension.
+-/
+import Lean
+
+open Lean Name
+
+inductive Extension where
+| html
+| pdf
+deriving Repr
+
+namespace Extension
+
+def cmp : Extension → Extension → Ordering
+ | html, html => Ordering.eq
+ | html, _ => Ordering.lt
+ | pdf, pdf => Ordering.eq
+ | pdf, _ => Ordering.gt
+
+instance : BEq Extension where
+ beq e1 e2 :=
+ match cmp e1 e2 with
+ | Ordering.eq => true
+ | _ => false
+
+def toString : Extension → String
+ | html => "html"
+ | pdf => "pdf"
+
+end Extension
+
+structure NameExt where
+ name : Name
+ ext : Extension
+
+namespace NameExt
+
+def cmp (n₁ n₂ : NameExt) : Ordering :=
+ match Name.cmp n₁.name n₂.name with
+ | Ordering.eq => Extension.cmp n₁.ext n₂.ext
+ | ord => ord
+
+def getString! : NameExt → String
+ | ⟨str _ s, _⟩ => s
+ | _ => unreachable!
+
+end NameExt