Add nameext to distinguish PDF and HTML files.

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.
 -/

DocGen4/Output/Navbar.lean

@@ -13,9 +13,14 @@ namespace Output
 open Lean
 open scoped DocGen4.Jsx
 
-def moduleListFile (file : Name) : BaseHtmlM Html := do
+def moduleListFile (file : NameExt) : BaseHtmlM Html := do
-  return <div class={if (← getCurrentName) == file then "nav_link visible" else "nav_link"}>
+  let contents :=
-    <a href={← moduleNameToLink file}>{file.getString!}</a>
+    if file.ext == .pdf then
+      <span>{s!"🗎 {file.getString!} (<a class=\"pdf\" target=\"_blank\" href={← moduleNameExtToLink file}>pdf</a>)"}</span>
+    else
+      <a href={← moduleNameExtToLink file}>{file.getString!}</a>
+  return <div class={if (← getCurrentName) == file.name then "nav_link visible" else "nav_link"}>
+    {contents}
   </div>
 
 /--
@@ -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 nodes ← children.mapM (fun c =>
-  let files := children.filter (fun c => Hierarchy.isFile c && c.getChildren.toList.length = 0)
+    if c.getChildren.toList.length != 0 then
-    |>.map Hierarchy.getName
+      moduleListDir c
-  let dirNodes ← dirs.mapM moduleListDir
+    else if Hierarchy.isFile c && c.getChildren.toList.length = 0 then
-  let fileNodes ← files.mapM moduleListFile
+      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
     <details class="nav_sect" "data-path"={moduleLink} [if (← getCurrentName).any (h.getName.isPrefixOf ·) then #[("open", "")] else #[]]>
       {summary}
-      [dirNodes]
+      [nodes]
-      [fileNodes]
     </details>
 
 /--

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

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
+partial def insert! (h : Hierarchy) (n : NameExt) : Hierarchy := Id.run do
-  let hn := h.getName
+  let hn := h.getNameExt
   let mut cs := h.getChildren
 
-  if getNumParts hn + 1 == getNumParts n then
+  if getNumParts hn.name + 1 == getNumParts n.name then
-    match cs.find Name.cmp n with
+    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
+        cs := cs.erase NameExt.cmp n
-        node hn h.isFile (cs.insert Name.cmp n <| node n true ccs)
+        node hn h.isFile (cs.insert NameExt.cmp n <| node n true ccs)
   else
-    let leveledName := getNLevels n (getNumParts hn + 1)
+    let leveledName := ⟨getNLevels n.name (getNumParts hn.name + 1), .html⟩
-    match cs.find Name.cmp leveledName with
+    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)
+        children := children.push <| ⟨.mkSimple (entry.fileName.dropRight ".html".length), .html⟩
-    return Hierarchy.fromArray children
+      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

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