diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean index 0776f61..7636deb 100644 --- a/DocGen4/Output.lean +++ b/DocGen4/Output.lean @@ -132,7 +132,7 @@ def getSimpleBaseContext (hierarchy : Hierarchy) : SiteBaseContext := hierarchy } -def htmlOutputFinalize (baseConfig : SiteBaseContext) : IO Unit := do +def htmlOutputIndex (baseConfig : SiteBaseContext) : IO Unit := do htmlOutputSetup baseConfig let mut topLevelModules := #[] @@ -151,7 +151,7 @@ The main entrypoint for outputting the documentation HTML based on an def htmlOutput (result : AnalyzerResult) (hierarchy : Hierarchy) (ws : Lake.Workspace) (inkPath : Option System.FilePath) : IO Unit := do let baseConfig := getSimpleBaseContext hierarchy htmlOutputResults baseConfig result ws inkPath - htmlOutputFinalize baseConfig + htmlOutputIndex baseConfig end DocGen4 diff --git a/Main.lean b/Main.lean index 2ea998e..a1bf44f 100644 --- a/Main.lean +++ b/Main.lean @@ -35,7 +35,7 @@ def runSingleCmd (p : Parsed) : IO UInt32 := do pure 0 | Except.error rc => pure rc -def runFinalizeCmd (p : Parsed) : IO UInt32 := do +def runIndexCmd (p : Parsed) : IO UInt32 := do let topLevelModules ← getTopLevelModules p let res ← lakeSetup topLevelModules match res with @@ -43,7 +43,7 @@ def runFinalizeCmd (p : Parsed) : IO UInt32 := do let modules := topLevelModules.map Name.mkSimple let hierarchy ← loadInit modules let baseConfig := getSimpleBaseContext hierarchy - htmlOutputFinalize baseConfig + htmlOutputIndex baseConfig pure 0 | Except.error rc => pure rc pure 0 @@ -76,9 +76,9 @@ def singleCmd := `[Cli| ...topLevelModules : String; "The top level modules this documentation will be for." ] -def finalizeCmd := `[Cli| - finalize VIA runFinalizeCmd; - "Finalize the documentation that has been generated by single." +def indexCmd := `[Cli| + index VIA runIndexCmd; + "Index the documentation that has been generated by single." ARGS: ...topLevelModule : String; "The top level modules this documentation will be for." ] @@ -95,7 +95,7 @@ def docGenCmd : Cmd := `[Cli| SUBCOMMANDS: singleCmd; - finalizeCmd + indexCmd ] def main (args : List String) : IO UInt32 := diff --git a/README.md b/README.md index f7c2146..38248c0 100644 --- a/README.md +++ b/README.md @@ -38,10 +38,10 @@ generate documentation for its first argument module. Furthermore one can use the `--ink` flag here to also generate LeanInk documentation in addition. -The second and last stage is the finalize one which zips up some +The second and last stage is the index one which zips up some information relevant for the search: ```sh -$ doc-gen4 finalize Mathlib +$ doc-gen4 index Mathlib ``` Now `build/doc` should contain the same files with the same context as if one had run ```