fix: adapt the rest of the program to the process refactor

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

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

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.

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
         </ul>
     </details>
 
-def classToHtml (i : ClassInfo) : HtmlM (Array Html) := do
+def classToHtml (i : Process.ClassInfo) : HtmlM (Array Html) := do
   pure $ (←structureToHtml i.toStructureInfo)
 
 end Output

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

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)

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

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 <li class="constructor" id={name}>{shortName} : [←infoFormatToHtml i.type]</li>
 
-def inductiveToHtml (i : InductiveInfo) : HtmlM (Array Html) := do
+def inductiveToHtml (i : Process.InductiveInfo) : HtmlM (Array Html) := do
   let constructorsHtml := <ul class="constructors">[← i.ctors.toArray.mapM ctorToHtml]</ul>
   pure #[constructorsHtml]
 

DocGen4/Output/Module.lean

@@ -11,13 +11,14 @@ import DocGen4.Output.Definition
 import DocGen4.Output.Instance
 import DocGen4.Output.ClassInductive
 import DocGen4.Output.DocString
+import DocGen4.Process
 import Lean.Data.Xml.Parser
 
 namespace DocGen4
 namespace Output
 
 open scoped DocGen4.Jsx
-open Lean
+open Lean Process
 
 /--
 Render an `Arg` as HTML, adding opacity effects etc. depending on what
@@ -45,7 +46,7 @@ def argToHtml (arg : Arg) : HtmlM Html := do
 Render the structures this structure extends from as HTML so it can be
 added to the top level.
 -/
-def structureInfoHeader (s : StructureInfo) : HtmlM (Array Html) := do
+def structureInfoHeader (s : Process.StructureInfo) : HtmlM (Array Html) := do
   let mut nodes := #[]
   if s.parents.size > 0 then
     nodes := nodes.push <span class="decl_extends">extends</span>
@@ -222,10 +223,10 @@ def internalNav (members : Array Name) (moduleName : Name) : HtmlM Html := do
 /--
 The main entry point to rendering the HTML for an entire module.
 -/
-def moduleToHtml (module : Module) : HtmlM Html := withReader (setCurrentName module.name) do
+def moduleToHtml (module : Process.Module) : HtmlM Html := withReader (setCurrentName module.name) do
   let memberDocs ← module.members.mapM (λ i => moduleMemberToHtml module.name i)
   let memberNames := filterMapDocInfo module.members |>.map DocInfo.getName
-  templateExtends (baseHtmlArray module.name.toString) $ pure #[
+  templateExtends (baseHtmlGenerator module.name.toString) $ pure #[
     ←internalNav memberNames module.name,
     Html.element "main" false #[] memberDocs
   ]

DocGen4/Output/Semantic.lean

@@ -1,8 +1,9 @@
 import DocGen4.Output.Template
 import DocGen4.Output.DocString
+import DocGen4.Process
 import Lean.Data.Xml
 
-open Lean Xml
+open Lean Xml DocGen4.Process
 
 namespace DocGen4
 namespace Output

DocGen4/Output/Structure.lean

@@ -1,5 +1,6 @@
 import DocGen4.Output.Template
 import DocGen4.Output.DocString
+import DocGen4.Process
 
 namespace DocGen4
 namespace Output
@@ -10,7 +11,7 @@ open Lean
 /--
 Render a single field consisting of its documentation, its name and its type as HTML.
 -/
-def fieldToHtml (f : NameInfo) : HtmlM Html := do
+def fieldToHtml (f : Process.NameInfo) : HtmlM Html := do
   let shortName := f.name.components'.head!.toString
   let name := f.name.toString
   if let some doc := f.doc then
@@ -29,7 +30,7 @@ def fieldToHtml (f : NameInfo) : HtmlM Html := do
 /--
 Render all information about a structure as HTML.
 -/
-def structureToHtml (i : StructureInfo) : HtmlM (Array Html) := do
+def structureToHtml (i : Process.StructureInfo) : HtmlM (Array Html) := do
   let structureHtml :=
     if Name.isSuffixOf `mk i.ctor.name then
       (<ul class="structure_fields" id={i.ctor.name.toString}>