bookshelf-doc/DocGen4/Output.lean

82 lines
3.4 KiB
Plaintext
Raw Normal View History

2021-12-12 12:21:53 +00:00
/-
Copyright (c) 2021 Henrik Böving. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
import Lean
2022-03-06 17:51:06 +00:00
import Lake
2021-12-12 12:21:53 +00:00
import DocGen4.Process
import DocGen4.Output.Base
import DocGen4.Output.Index
import DocGen4.Output.Module
import DocGen4.Output.NotFound
2022-02-13 14:42:15 +00:00
import DocGen4.Output.Find
2022-02-22 20:26:20 +00:00
import DocGen4.Output.Semantic
import DocGen4.Output.SourceLinker
2021-12-12 12:21:53 +00:00
namespace DocGen4
open Lean IO System Output Process
2021-12-13 12:00:53 +00:00
2022-05-19 18:54:42 +00:00
/--
The main entrypoint for outputting the documentation HTML based on an
`AnalyzerResult`.
-/
2022-04-06 23:31:27 +00:00
def htmlOutput (result : AnalyzerResult) (ws : Lake.Workspace) (leanHash: String) : IO Unit := do
let config : SiteContext := { depthToRoot := 0, result := result, currentName := none, sourceLinker := ←sourceLinker ws leanHash}
let basePath := FilePath.mk "." / "build" / "doc"
let indexHtml := ReaderT.run index config
2022-04-07 11:14:01 +00:00
let findHtml := ReaderT.run find { config with depthToRoot := 1 }
let notFoundHtml := ReaderT.run notFound config
2022-02-13 14:42:15 +00:00
FS.createDirAll basePath
FS.createDirAll (basePath / "find")
2022-02-22 20:26:20 +00:00
FS.createDirAll (basePath / "semantic")
2022-02-13 14:42:15 +00:00
2022-02-13 14:03:49 +00:00
let mut declList := #[]
2022-04-06 23:53:06 +00:00
for (_, mod) in result.moduleInfo.toArray do
2022-02-18 04:52:01 +00:00
for decl in filterMapDocInfo mod.members do
2022-02-20 17:12:49 +00:00
let name := decl.getName.toString
2022-04-07 10:44:33 +00:00
let config := { config with depthToRoot := 0 }
2022-02-22 07:01:14 +00:00
let doc := decl.getDocString.getD ""
2022-04-06 23:31:27 +00:00
let root := Id.run <| ReaderT.run (getRoot) config
let link := root ++ s!"../semantic/{decl.getName.hash}.xml#"
2022-02-22 20:26:20 +00:00
let docLink := Id.run <| ReaderT.run (declNameToLink decl.getName) config
let sourceLink := Id.run <| ReaderT.run (getSourceUrl mod.name decl.getDeclarationRange) config
2022-02-22 21:32:37 +00:00
let obj := Json.mkObj [("name", name), ("doc", doc), ("link", link), ("docLink", docLink), ("sourceLink", sourceLink)]
2022-02-13 14:03:49 +00:00
declList := declList.push obj
2022-02-22 20:26:20 +00:00
let xml := toString <| Id.run <| ReaderT.run (semanticXml decl) config
FS.writeFile (basePath / "semantic" / s!"{decl.getName.hash}.xml") xml
2022-02-13 14:03:49 +00:00
let json := Json.arr declList
2022-02-13 14:42:15 +00:00
2022-02-22 20:26:20 +00:00
FS.writeFile (basePath / "semantic" / "docgen4.xml") <| toString <| Id.run <| ReaderT.run schemaXml config
2021-12-12 12:21:53 +00:00
FS.writeFile (basePath / "index.html") indexHtml.toString
2021-12-13 12:00:53 +00:00
FS.writeFile (basePath / "404.html") notFoundHtml.toString
2022-02-22 04:40:14 +00:00
FS.writeFile (basePath / "find" / "index.html") findHtml.toString
FS.writeFile (basePath / "style.css") styleCss
let declarationDataPath := basePath / "declaration-data.bmp"
FS.writeFile declarationDataPath json.compress
FS.writeFile (basePath / "declaration-data.timestamp") <| toString (←declarationDataPath.metadata).modified.sec
FS.writeFile (basePath / "declaration-data.js") declarationDataCenterJs
FS.writeFile (basePath / "nav.js") navJs
2022-02-22 04:40:14 +00:00
FS.writeFile (basePath / "find" / "find.js") findJs
FS.writeFile (basePath / "how-about.js") howAboutJs
2022-02-13 13:25:37 +00:00
FS.writeFile (basePath / "search.js") searchJs
2022-02-17 19:27:00 +00:00
FS.writeFile (basePath / "mathjax-config.js") mathjaxConfigJs
2022-02-20 17:12:49 +00:00
2021-12-17 16:20:44 +00:00
for (module, content) in result.moduleInfo.toArray do
let fileDir := moduleNameToDirectory basePath module
let filePath := moduleNameToFile basePath module
-- path: 'basePath/module/components/till/last.html'
-- The last component is the file name, so we drop it from the depth to root.
let config := { config with depthToRoot := module.components.dropLast.length }
2021-12-13 12:00:53 +00:00
let moduleHtml := ReaderT.run (moduleToHtml content) config
FS.createDirAll $ fileDir
FS.writeFile filePath moduleHtml.toString
2021-12-12 12:21:53 +00:00
end DocGen4