feat: index shall not depend on importing things

main
Henrik Böving 2022-07-22 00:34:13 +02:00
parent c35d750e67
commit c29cf7b70c
3 changed files with 43 additions and 17 deletions

View File

@ -12,14 +12,9 @@ import DocGen4.Process.Base
import DocGen4.Process.Hierarchy import DocGen4.Process.Hierarchy
import DocGen4.Process.DocInfo import DocGen4.Process.DocInfo
open Std
def HashSet.fromArray [BEq α] [Hashable α] (xs : Array α) : HashSet α :=
xs.foldr (flip .insert) .empty
namespace DocGen4.Process namespace DocGen4.Process
open Lean Meta open Lean Meta Std
/-- /--
Member of a module, either a declaration or some module doc string. Member of a module, either a declaration or some module doc string.

View File

@ -6,9 +6,14 @@ Authors: Henrik Böving
import Lean import Lean
import Std.Data.HashMap import Std.Data.HashMap
open Std
def HashSet.fromArray [BEq α] [Hashable α] (xs : Array α) : HashSet α :=
xs.foldr (flip .insert) .empty
namespace DocGen4 namespace DocGen4
open Lean Std Name open Lean Name
def getNLevels (name : Name) (levels: Nat) : Name := def getNLevels (name : Name) (levels: Nat) : Name :=
let components := name.components' 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 := partial def fromArray (names : Array Name) : Hierarchy :=
names.foldl insert! (empty anonymous false) 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 Hierarchy
end DocGen4 end DocGen4

View File

@ -34,16 +34,9 @@ def runSingleCmd (p : Parsed) : IO UInt32 := do
| Except.error rc => pure rc | Except.error rc => pure rc
def runIndexCmd (p : Parsed) : IO UInt32 := do def runIndexCmd (p : Parsed) : IO UInt32 := do
let topLevelModules ← getTopLevelModules p let hierarchy ← Hierarchy.fromDirectory basePath
let res ← lakeSetup topLevelModules let baseConfig := getSimpleBaseContext hierarchy
match res with htmlOutputIndex baseConfig
| 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
pure 0 pure 0
def runDocGenCmd (p : Parsed) : IO UInt32 := do def runDocGenCmd (p : Parsed) : IO UInt32 := do