diff --git a/DocGen4/Process/Analyze.lean b/DocGen4/Process/Analyze.lean index 1ec0e7c..77469af 100644 --- a/DocGen4/Process/Analyze.lean +++ b/DocGen4/Process/Analyze.lean @@ -12,14 +12,9 @@ import DocGen4.Process.Base import DocGen4.Process.Hierarchy import DocGen4.Process.DocInfo -open Std - -def HashSet.fromArray [BEq α] [Hashable α] (xs : Array α) : HashSet α := - xs.foldr (flip .insert) .empty - namespace DocGen4.Process -open Lean Meta +open Lean Meta Std /-- Member of a module, either a declaration or some module doc string. diff --git a/DocGen4/Process/Hierarchy.lean b/DocGen4/Process/Hierarchy.lean index 32b2805..7727e15 100644 --- a/DocGen4/Process/Hierarchy.lean +++ b/DocGen4/Process/Hierarchy.lean @@ -6,9 +6,14 @@ Authors: Henrik Böving import Lean import Std.Data.HashMap +open Std + +def HashSet.fromArray [BEq α] [Hashable α] (xs : Array α) : HashSet α := + xs.foldr (flip .insert) .empty + namespace DocGen4 -open Lean Std Name +open Lean Name def getNLevels (name : Name) (levels: Nat) : Name := let components := name.components' @@ -78,5 +83,38 @@ partial def insert! (h : Hierarchy) (n : Name) : Hierarchy := Id.run $ do partial def fromArray (names : Array Name) : Hierarchy := names.foldl insert! (empty anonymous false) +def baseDirBlackList : HashSet String := + HashSet.fromArray #[ + "404.html", + "declaration-data.js", + "declarations", + "find", + "how-about.js", + "index.html", + "mathjax-config.js", + "navbar.html", + "nav.js", + "search.js", + "src", + "style.css" + ] + + +partial def fromDirectoryAux (dir : System.FilePath) (previous : Name) : IO (Array Name) := 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 + children := children.push $ .str previous (entry.fileName.dropRight ".html".length) + pure children + +def fromDirectory (dir : System.FilePath) : IO Hierarchy := do + let mut children := #[] + for entry in ←System.FilePath.readDir dir do + if !baseDirBlackList.contains entry.fileName && (←entry.path.isDir) then + children := children ++ (←fromDirectoryAux entry.path (.mkSimple entry.fileName)) + pure $ Hierarchy.fromArray children + end Hierarchy end DocGen4 diff --git a/Main.lean b/Main.lean index 2005c19..f514be6 100644 --- a/Main.lean +++ b/Main.lean @@ -34,16 +34,9 @@ def runSingleCmd (p : Parsed) : IO UInt32 := do | Except.error rc => pure rc def runIndexCmd (p : Parsed) : IO UInt32 := do - let topLevelModules ← getTopLevelModules p - let res ← lakeSetup topLevelModules - match res with - | Except.ok _ => - let modules := topLevelModules.map String.toName - let hierarchy ← loadInit modules - let baseConfig := getSimpleBaseContext hierarchy - htmlOutputIndex baseConfig - pure 0 - | Except.error rc => pure rc + let hierarchy ← Hierarchy.fromDirectory basePath + let baseConfig := getSimpleBaseContext hierarchy + htmlOutputIndex baseConfig pure 0 def runDocGenCmd (p : Parsed) : IO UInt32 := do