bookshelf/DocGen4/LeanInk/Process.lean

58 lines
1.8 KiB
Plaintext
Raw Normal View History

2023-05-11 13:27:25 +00:00
/-
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