r
/
bookshelf-doc
mirror of https://github.com/jrpotter/bookshelf-doc
1
Fork 0
Code Issues Packages Projects Releases Wiki Activity

feat: Renamed finalize to index

main
Henrik Böving 2022-07-21 21:12:15 +02:00
parent 71af8db54b
commit 80cf5bc96f
3 changed files with 10 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
DocGen4/Output.lean
View File

@ -132,7 +132,7 @@ def getSimpleBaseContext (hierarchy : Hierarchy) : SiteBaseContext :=
hierarchy hierarchy
} }
def htmlOutputFinalize (baseConfig : SiteBaseContext) : IO Unit := do def htmlOutputIndex (baseConfig : SiteBaseContext) : IO Unit := do
htmlOutputSetup baseConfig htmlOutputSetup baseConfig
let mut topLevelModules := #[] 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 def htmlOutput (result : AnalyzerResult) (hierarchy : Hierarchy) (ws : Lake.Workspace) (inkPath : Option System.FilePath) : IO Unit := do
let baseConfig := getSimpleBaseContext hierarchy let baseConfig := getSimpleBaseContext hierarchy
htmlOutputResults baseConfig result ws inkPath htmlOutputResults baseConfig result ws inkPath
htmlOutputFinalize baseConfig htmlOutputIndex baseConfig
end DocGen4 end DocGen4

12
Main.lean
View File

@ -35,7 +35,7 @@ def runSingleCmd (p : Parsed) : IO UInt32 := do
pure 0 pure 0
| Except.error rc => pure rc | Except.error rc => pure rc
def runFinalizeCmd (p : Parsed) : IO UInt32 := do def runIndexCmd (p : Parsed) : IO UInt32 := do
let topLevelModules ← getTopLevelModules p let topLevelModules ← getTopLevelModules p
let res ← lakeSetup topLevelModules let res ← lakeSetup topLevelModules
match res with match res with
@ -43,7 +43,7 @@ def runFinalizeCmd (p : Parsed) : IO UInt32 := do
let modules := topLevelModules.map Name.mkSimple let modules := topLevelModules.map Name.mkSimple
let hierarchy ← loadInit modules let hierarchy ← loadInit modules
let baseConfig := getSimpleBaseContext hierarchy let baseConfig := getSimpleBaseContext hierarchy
htmlOutputFinalize baseConfig htmlOutputIndex baseConfig
pure 0 pure 0
| Except.error rc => pure rc | Except.error rc => pure rc
pure 0 pure 0
@ -76,9 +76,9 @@ def singleCmd := `[Cli|
...topLevelModules : String; "The top level modules this documentation will be for." ...topLevelModules : String; "The top level modules this documentation will be for."
] ]
def finalizeCmd := `[Cli| def indexCmd := `[Cli|
finalize VIA runFinalizeCmd; index VIA runIndexCmd;
"Finalize the documentation that has been generated by single." "Index the documentation that has been generated by single."
ARGS: ARGS:
...topLevelModule : String; "The top level modules this documentation will be for." ...topLevelModule : String; "The top level modules this documentation will be for."
] ]
@ -95,7 +95,7 @@ def docGenCmd : Cmd := `[Cli|
SUBCOMMANDS: SUBCOMMANDS:
singleCmd; singleCmd;
finalizeCmd indexCmd
] ]
def main (args : List String) : IO UInt32 := def main (args : List String) : IO UInt32 :=

4
README.md
View File

@ -38,10 +38,10 @@ generate documentation for its first argument module.
Furthermore one can use the `--ink` flag here to also generate LeanInk Furthermore one can use the `--ink` flag here to also generate LeanInk
documentation in addition. 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: information relevant for the search:
```sh ```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 Now `build/doc` should contain the same files with the same context as if one had run
``` ```