feat: Degrade --ink to flag
parent
5a893f4b76
commit
14afcdbeaf
|
@ -72,11 +72,11 @@ def htmlOutputDeclarationDatas (result : AnalyzerResult) : HtmlT IO Unit := do
|
|||
let jsonDecls ← Module.toJson mod
|
||||
FS.writeFile (declarationsBasePath / s!"declaration-data-{mod.name}.bmp") (toJson jsonDecls).compress
|
||||
|
||||
def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) (ws : Lake.Workspace) (inkPath : Option System.FilePath) : IO Unit := do
|
||||
def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) (ws : Lake.Workspace) (ink : Bool) : IO Unit := do
|
||||
let config : SiteContext := {
|
||||
result := result,
|
||||
sourceLinker := ←sourceLinker ws
|
||||
leanInkEnabled := inkPath.isSome
|
||||
leanInkEnabled := ink
|
||||
}
|
||||
|
||||
FS.createDirAll basePath
|
||||
|
@ -100,7 +100,7 @@ def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) (
|
|||
let moduleHtml := moduleToHtml module |>.run config baseConfig
|
||||
FS.createDirAll fileDir
|
||||
FS.writeFile filePath moduleHtml.toString
|
||||
if let some inkPath := inkPath then
|
||||
if ink then
|
||||
if let some inputPath ← Lean.SearchPath.findModuleWithExt sourceSearchPath "lean" module.name then
|
||||
IO.println s!"Inking: {modName.toString}"
|
||||
-- path: 'basePath/src/module/components/till/last.html'
|
||||
|
@ -134,9 +134,9 @@ def htmlOutputIndex (baseConfig : SiteBaseContext) : IO Unit := do
|
|||
The main entrypoint for outputting the documentation HTML based on an
|
||||
`AnalyzerResult`.
|
||||
-/
|
||||
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) (ink : Bool) : IO Unit := do
|
||||
let baseConfig := getSimpleBaseContext hierarchy
|
||||
htmlOutputResults baseConfig result ws inkPath
|
||||
htmlOutputResults baseConfig result ws ink
|
||||
htmlOutputIndex baseConfig
|
||||
|
||||
end DocGen4
|
||||
|
|
18
Main.lean
18
Main.lean
|
@ -4,16 +4,6 @@ import Cli
|
|||
|
||||
open DocGen4 Lean Cli
|
||||
|
||||
def findLeanInk? (p : Parsed) : IO (Option System.FilePath) := do
|
||||
match p.flag? "ink" with
|
||||
| some ink =>
|
||||
let inkPath := System.FilePath.mk ink.value
|
||||
if ←inkPath.pathExists then
|
||||
pure <| some inkPath
|
||||
else
|
||||
throw <| IO.userError "Invalid path to LeanInk binary provided"
|
||||
| none => pure none
|
||||
|
||||
def getTopLevelModules (p : Parsed) : IO (List String) := do
|
||||
let topLevelModules := p.variableArgsAs! String |>.toList
|
||||
if topLevelModules.length == 0 then
|
||||
|
@ -29,7 +19,7 @@ def runSingleCmd (p : Parsed) : IO UInt32 := do
|
|||
let (doc, hierarchy) ← load (.loadAllLimitAnalysis relevantModules)
|
||||
IO.println "Outputting HTML"
|
||||
let baseConfig := getSimpleBaseContext hierarchy
|
||||
htmlOutputResults baseConfig doc ws (←findLeanInk? p)
|
||||
htmlOutputResults baseConfig doc ws (p.hasFlag "ink")
|
||||
pure 0
|
||||
| Except.error rc => pure rc
|
||||
|
||||
|
@ -51,7 +41,7 @@ def runDocGenCmd (p : Parsed) : IO UInt32 := do
|
|||
let modules := modules.map String.toName
|
||||
let (doc, hierarchy) ← load (.loadAll modules)
|
||||
IO.println "Outputting HTML"
|
||||
htmlOutput doc hierarchy ws (←findLeanInk? p)
|
||||
htmlOutput doc hierarchy ws (p.hasFlag "ink")
|
||||
pure 0
|
||||
| Except.error rc => pure rc
|
||||
|
||||
|
@ -60,7 +50,7 @@ def singleCmd := `[Cli|
|
|||
"Only generate the documentation for the module it was given, might contain broken links unless all documentation is generated."
|
||||
|
||||
FLAGS:
|
||||
ink : String; "Path to a LeanInk binary to use for rendering the Lean sources."
|
||||
ink; "Render the files with LeanInk in addition"
|
||||
|
||||
ARGS:
|
||||
module : String; "The module to generate the HTML for. Does not have to be part of topLevelModules."
|
||||
|
@ -78,7 +68,7 @@ def docGenCmd : Cmd := `[Cli|
|
|||
"A documentation generator for Lean 4."
|
||||
|
||||
FLAGS:
|
||||
ink : String; "Path to a LeanInk binary to use for rendering the Lean sources."
|
||||
ink; "Render the files with LeanInk in addition"
|
||||
|
||||
ARGS:
|
||||
...modules : String; "The modules to generate the HTML for."
|
||||
|
|
Loading…
Reference in New Issue