diff --git a/DocGen4/Load.lean b/DocGen4/Load.lean index e86694b..09d2d5c 100644 --- a/DocGen4/Load.lean +++ b/DocGen4/Load.lean @@ -37,10 +37,10 @@ def lakeSetup (imports : List String) : IO (Except UInt32 (Lake.Workspace × Str Load a list of modules from the current Lean search path into an `Environment` to process for documentation. -/ -def load (imports : List Name) : IO AnalyzerResult := do +def load (imports : List Name) : IO Process.AnalyzerResult := do let env ← importModules (List.map (Import.mk · false) imports) Options.empty -- TODO parameterize maxHeartbeats IO.println "Processing modules" - Prod.fst <$> Meta.MetaM.toIO process { maxHeartbeats := 100000000, options := ⟨[(`pp.tagAppFns, true)]⟩ } { env := env} {} {} + Prod.fst <$> Meta.MetaM.toIO Process.process { maxHeartbeats := 100000000, options := ⟨[(`pp.tagAppFns, true)]⟩ } { env := env} {} {} end DocGen4 diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index feedfda..59ad9e7 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -16,7 +16,7 @@ import DocGen4.Output.SourceLinker namespace DocGen4 -open Lean IO System Output +open Lean IO System Output Process /-- The main entrypoint for outputting the documentation HTML based on an diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean index cdcbca6..795daa8 100644 --- a/DocGen4/Output/Base.lean +++ b/DocGen4/Output/Base.lean @@ -10,7 +10,7 @@ import DocGen4.Output.ToHtmlFormat namespace DocGen4.Output open scoped DocGen4.Jsx -open Lean System Widget Elab +open Lean System Widget Elab Process /-- The context used in the `HtmlM` monad for HTML templating. diff --git a/DocGen4/Output/Class.lean b/DocGen4/Output/Class.lean index e39a424..5ca853e 100644 --- a/DocGen4/Output/Class.lean +++ b/DocGen4/Output/Class.lean @@ -1,5 +1,6 @@ import DocGen4.Output.Template import DocGen4.Output.Structure +import DocGen4.Process namespace DocGen4 namespace Output @@ -20,7 +21,7 @@ def classInstancesToHtml (instances : Array Name) : HtmlM Html := do -def classToHtml (i : ClassInfo) : HtmlM (Array Html) := do +def classToHtml (i : Process.ClassInfo) : HtmlM (Array Html) := do pure $ (←structureToHtml i.toStructureInfo) end Output diff --git a/DocGen4/Output/ClassInductive.lean b/DocGen4/Output/ClassInductive.lean index 140651e..7b8ab24 100644 --- a/DocGen4/Output/ClassInductive.lean +++ b/DocGen4/Output/ClassInductive.lean @@ -1,12 +1,13 @@ import DocGen4.Output.Template import DocGen4.Output.Class import DocGen4.Output.Inductive +import DocGen4.Process namespace DocGen4 namespace Output -def classInductiveToHtml (i : ClassInductiveInfo) : HtmlM (Array Html) := do +def classInductiveToHtml (i : Process.ClassInductiveInfo) : HtmlM (Array Html) := do pure $ (←inductiveToHtml i.toInductiveInfo) end Output diff --git a/DocGen4/Output/Definition.lean b/DocGen4/Output/Definition.lean index 6be1639..4b4e280 100644 --- a/DocGen4/Output/Definition.lean +++ b/DocGen4/Output/Definition.lean @@ -1,5 +1,6 @@ import DocGen4.Output.Template import DocGen4.Output.DocString +import DocGen4.Process namespace DocGen4 namespace Output @@ -19,7 +20,7 @@ defined in `equationLimit` we stop trying since they: - are too ugly to read most of the time - take too long -/ -def equationsToHtml (i : DefinitionInfo) : HtmlM (Array Html) := do +def equationsToHtml (i : Process.DefinitionInfo) : HtmlM (Array Html) := do if let some eqs := i.equations then let equationsHtml ← eqs.mapM equationToHtml let filteredEquationsHtml := equationsHtml.filter (λ eq => eq.textLength < equationLimit) diff --git a/DocGen4/Output/DocString.lean b/DocGen4/Output/DocString.lean index d729d38..d1506ab 100644 --- a/DocGen4/Output/DocString.lean +++ b/DocGen4/Output/DocString.lean @@ -3,7 +3,7 @@ import DocGen4.Output.Template import Lean.Data.Parsec import Unicode.General.GeneralCategory -open Lean Unicode Xml Parser Parsec +open Lean Unicode Xml Parser Parsec DocGen4.Process namespace DocGen4 namespace Output diff --git a/DocGen4/Output/Inductive.lean b/DocGen4/Output/Inductive.lean index 419891d..4a73bd3 100644 --- a/DocGen4/Output/Inductive.lean +++ b/DocGen4/Output/Inductive.lean @@ -1,17 +1,18 @@ import DocGen4.Output.Template import DocGen4.Output.DocString +import DocGen4.Process namespace DocGen4 namespace Output open scoped DocGen4.Jsx -def ctorToHtml (i : NameInfo) : HtmlM Html := do +def ctorToHtml (i : Process.NameInfo) : HtmlM Html := do let shortName := i.name.components'.head!.toString let name := i.name.toString pure