48 lines
1.3 KiB
Plaintext
48 lines
1.3 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),
|
||
(`pp.funBinderTypes, true)
|
||
]⟩,
|
||
-- TODO: Figure out whether this could cause some bugs
|
||
fileName := default,
|
||
fileMap := default,
|
||
catchRuntimeEx := true,
|
||
}
|
||
|
||
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
|