58 lines
1.8 KiB
Plaintext
58 lines
1.8 KiB
Plaintext
|
/-
|
||
|
|
Copyright (c) 2022 Henrik Böving. All rights reserved.
|
||
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
||
|
|
Authors: Henrik Böving
|
||
|
|
-/
|
||
|
|
import Lean
|
||
|
|
import LeanInk.Analysis
|
||
|
|
import LeanInk.Annotation
|
||
|
|
import DocGen4.LeanInk.Output
|
||
|
|
import DocGen4.Output.Base
|
||
|
|
|
||
|
|
namespace DocGen4.Process.LeanInk
|
||
|
|
|
||
|
|
open Lean
|
||
|
|
open DocGen4.Output
|
||
|
|
|
||
|
|
def docGenOutput (as : List LeanInk.Annotation.Annotation) : HtmlT LeanInk.AnalysisM UInt32 := do
|
||
|
|
let some modName ← getCurrentName | unreachable!
|
||
|
|
let srcHtml ← LeanInk.Annotation.Alectryon.renderAnnotations as
|
||
|
|
let srcDir := moduleNameToDirectory srcBasePath modName
|
||
|
|
let srcPath := moduleNameToFile srcBasePath modName
|
||
|
|
IO.FS.createDirAll srcDir
|
||
|
|
IO.FS.writeFile srcPath srcHtml.toString
|
||
|
|
return 0
|
||
|
|
|
||
|
|
def execAuxM : HtmlT LeanInk.AnalysisM UInt32 := do
|
||
|
|
let ctx ← readThe SiteContext
|
||
|
|
let baseCtx ← readThe SiteBaseContext
|
||
|
|
let outputFn := (docGenOutput · |>.run ctx baseCtx)
|
||
|
|
return ← LeanInk.Analysis.runAnalysis {
|
||
|
|
name := "doc-gen4"
|
||
|
|
genOutput := outputFn
|
||
|
|
}
|
||
|
|
|
||
|
|
def execAux (config : LeanInk.Configuration) : HtmlT IO UInt32 := do
|
||
|
|
execAuxM.run (← readThe SiteContext) (← readThe SiteBaseContext) |>.run config
|
||
|
|
|
||
|
|
@[implemented_by enableInitializersExecution]
|
||
|
|
private def enableInitializersExecutionWrapper : IO Unit := return ()
|
||
|
|
|
||
|
|
def runInk (sourceFilePath : System.FilePath) : HtmlT IO Unit := do
|
||
|
|
let contents ← IO.FS.readFile sourceFilePath
|
||
|
|
let config := {
|
||
|
|
inputFilePath := sourceFilePath
|
||
|
|
inputFileContents := contents
|
||
|
|
lakeFile := none
|
||
|
|
verbose := false
|
||
|
|
prettifyOutput := true
|
||
|
|
experimentalTypeInfo := true
|
||
|
|
experimentalDocString := true
|
||
|
|
experimentalSemanticType := true
|
||
|
|
}
|
||
|
|
enableInitializersExecutionWrapper
|
||
|
|
if (← execAux config) != 0 then
|
||
|
|
throw <| IO.userError s!"Analysis for \"{sourceFilePath}\" failed!"
|
||
|
|
|
||
|
|
end DocGen4.Process.LeanInk
|