44 lines
1.2 KiB
Plaintext
44 lines
1.2 KiB
Plaintext
/-
|
||
Copyright (c) 2021 Henrik Böving. All rights reserved.
|
||
Released under Apache 2.0 license as described in the file LICENSE.
|
||
Authors: Henrik Böving
|
||
-/
|
||
|
||
import Lean
|
||
import DocGen4.Process
|
||
import Lean.Data.HashMap
|
||
|
||
namespace DocGen4
|
||
|
||
open Lean System IO
|
||
|
||
def envOfImports (imports : Array Name) : IO Environment := do
|
||
importModules (imports.map (Import.mk · false)) Options.empty
|
||
|
||
def loadInit (imports : Array Name) : IO Hierarchy := do
|
||
let env ← envOfImports imports
|
||
pure <| Hierarchy.fromArray env.header.moduleNames
|
||
|
||
/--
|
||
Load a list of modules from the current Lean search path into an `Environment`
|
||
to process for documentation.
|
||
-/
|
||
def load (task : Process.AnalyzeTask) : IO (Process.AnalyzerResult × Hierarchy) := do
|
||
initSearchPath (← findSysroot)
|
||
let env ← envOfImports task.getLoad
|
||
let config := {
|
||
-- TODO: parameterize maxHeartbeats
|
||
maxHeartbeats := 100000000,
|
||
options := ⟨[(`pp.tagAppFns, true)]⟩,
|
||
-- TODO: Figure out whether this could cause some bugs
|
||
fileName := default,
|
||
fileMap := default,
|
||
}
|
||
|
||
Prod.fst <$> Meta.MetaM.toIO (Process.process task) config { env := env } {} {}
|
||
|
||
def loadCore : IO (Process.AnalyzerResult × Hierarchy) := do
|
||
load <| .loadAll #[`Init, `Lean, `Lake]
|
||
|
||
end DocGen4
|