bookshelf-doc/DocGen4/Output/Base.lean

255 lines
9.3 KiB
Plaintext
Raw Normal View History

/-
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 DocGen4.Process
2022-05-19 18:36:35 +00:00
import DocGen4.Output.ToHtmlFormat
2022-05-19 19:05:17 +00:00
namespace DocGen4.Output
open scoped DocGen4.Jsx
open Lean System Widget Elab Process
2022-07-26 10:52:41 +00:00
def basePath := FilePath.mk "." / "build" / "doc"
def srcBasePath := basePath / "src"
def declarationsBasePath := basePath / "declarations"
2022-05-19 19:05:17 +00:00
/--
The context used in the `BaseHtmlM` monad for HTML templating.
2022-05-19 19:05:17 +00:00
-/
structure SiteBaseContext where
2022-05-19 19:05:17 +00:00
/--
The module hierarchy as a tree structure.
2022-05-19 19:05:17 +00:00
-/
hierarchy : Hierarchy
2022-05-19 19:05:17 +00:00
/--
How far away we are from the page root, used for relative links to the root.
-/
depthToRoot: Nat
2022-05-19 19:05:17 +00:00
/--
The name of the current module if there is one, there exist a few
pages that don't have a module name.
-/
currentName : Option Name
/--
The context used in the `HtmlM` monad for HTML templating.
-/
structure SiteContext where
/--
The full analysis result from the Process module.
-/
result : AnalyzerResult
2022-05-19 19:05:17 +00:00
/--
A function to link declaration names to their source URLs, usually Github ones.
-/
2022-01-09 15:57:19 +00:00
sourceLinker : Name → Option DeclarationRange → String
/--
Whether LeanInk is enabled
-/
leanInkEnabled : Bool
def setCurrentName (name : Name) (ctx : SiteBaseContext) := {ctx with currentName := some name}
abbrev BaseHtmlT := ReaderT SiteBaseContext
abbrev BaseHtmlM := BaseHtmlT Id
abbrev HtmlT (m) := ReaderT SiteContext (BaseHtmlT m)
abbrev HtmlM := HtmlT Id
def HtmlT.run (x : HtmlT m α) (ctx : SiteContext) (baseCtx : SiteBaseContext) : m α :=
ReaderT.run x ctx |>.run baseCtx
def HtmlM.run (x : HtmlM α) (ctx : SiteContext) (baseCtx : SiteBaseContext) : α :=
ReaderT.run x ctx |>.run baseCtx |>.run
instance [Monad m] : MonadLift HtmlM (HtmlT m) where
monadLift x := do pure <| x.run (←readThe SiteContext) (←readThe SiteBaseContext)
instance [Monad m] : MonadLift BaseHtmlM (BaseHtmlT m) where
monadLift x := do pure <| x.run (←readThe SiteBaseContext)
2022-05-19 19:05:17 +00:00
/--
Obtains the root URL as a relative one to the current depth.
-/
def getRoot : BaseHtmlM String := do
let rec go: Nat -> String
| 0 => "./"
| Nat.succ n' => "../" ++ go n'
let d <- SiteBaseContext.depthToRoot <$> read
return (go d)
def getHierarchy : BaseHtmlM Hierarchy := do pure (←read).hierarchy
def getCurrentName : BaseHtmlM (Option Name) := do pure (←read).currentName
2022-02-12 14:09:13 +00:00
def getResult : HtmlM AnalyzerResult := do pure (←read).result
2022-07-23 11:01:25 +00:00
def getSourceUrl (module : Name) (range : Option DeclarationRange): HtmlM String := do pure <| (←read).sourceLinker module range
def leanInkEnabled? : HtmlM Bool := do pure (←read).leanInkEnabled
2022-05-19 19:05:17 +00:00
/--
If a template is meant to be extended because it for example only provides the
header but no real content this is the way to fill the template with content.
This is untyped so HtmlM and BaseHtmlM can be mixed.
2022-05-19 19:05:17 +00:00
-/
def templateExtends {α β} {m} [Bind m] (base : α → m β) (new : m α) : m β :=
new >>= base
def templateLiftExtends {α β} {m n} [Bind m] [MonadLift n m] (base : α → n β) (new : m α) : m β :=
new >>= (monadLift ∘ base)
2022-05-19 19:05:17 +00:00
/--
Returns the doc-gen4 link to a module name.
-/
def moduleNameToLink (n : Name) : BaseHtmlM String := do
2021-12-17 16:20:44 +00:00
let parts := n.components.map Name.toString
2022-07-23 11:01:25 +00:00
pure <| (← getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html"
/--
Returns the HTML doc-gen4 link to a module name.
-/
def moduleToHtmlLink (module : Name) : BaseHtmlM Html := do
pure <a href={←moduleNameToLink module}>{module.toString}</a>
/--
Returns the LeanInk link to a module name.
-/
def moduleNameToInkLink (n : Name) : BaseHtmlM String := do
let parts := "src" :: n.components.map Name.toString
2022-07-23 11:01:25 +00:00
pure <| (← getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html"
2022-05-19 19:05:17 +00:00
/--
Returns the path to the HTML file that contains information about a module.
-/
2021-12-15 10:59:13 +00:00
def moduleNameToFile (basePath : FilePath) (n : Name) : FilePath :=
2022-01-15 14:35:52 +00:00
let parts := n.components.map Name.toString
FilePath.withExtension (basePath / parts.foldl (· / ·) (FilePath.mk ".")) "html"
2021-12-15 10:59:13 +00:00
2022-05-19 19:05:17 +00:00
/--
Returns the directory of the HTML file that contains information about a module.
-/
2021-12-15 10:59:13 +00:00
def moduleNameToDirectory (basePath : FilePath) (n : Name) : FilePath :=
2022-01-15 14:35:52 +00:00
let parts := n.components.dropLast.map Name.toString
basePath / parts.foldl (· / ·) (FilePath.mk ".")
section Static
2022-05-19 19:05:17 +00:00
/-!
The following section contains all the statically included files that
are used in documentation generation, notably JS and CSS ones.
-/
def styleCss : String := include_str "../../static/style.css"
def declarationDataCenterJs : String := include_str "../../static/declaration-data.js"
def navJs : String := include_str "../../static/nav.js"
def howAboutJs : String := include_str "../../static/how-about.js"
def searchJs : String := include_str "../../static/search.js"
def instancesJs : String := include_str "../../static/instances.js"
2022-07-22 14:15:37 +00:00
def importedByJs : String := include_str "../../static/importedBy.js"
def findJs : String := include_str "../../static/find/find.js"
def mathjaxConfigJs : String := include_str "../../static/mathjax-config.js"
2022-06-20 16:39:55 +00:00
def alectryonCss : String := include_str "../../static/alectryon/alectryon.css"
def alectryonJs : String := include_str "../../static/alectryon/alectryon.js"
def docUtilsCss : String := include_str "../../static/alectryon/docutils_basic.css"
def pygmentsCss : String := include_str "../../static/alectryon/pygments.css"
end Static
2022-05-19 19:05:17 +00:00
/--
Returns the doc-gen4 link to a declaration name.
-/
def declNameToLink (name : Name) : HtmlM String := do
let res ← getResult
2022-07-20 14:18:57 +00:00
let module := res.moduleNames[res.name2ModIdx.find! name |>.toNat]!
2022-07-23 11:01:25 +00:00
pure <| (←moduleNameToLink module) ++ "#" ++ name.toString
/--
Returns the HTML doc-gen4 link to a declaration name.
-/
def declNameToHtmlLink (name : Name) : HtmlM Html := do
pure <a href={←declNameToLink name}>{name.toString}</a>
/--
Returns the LeanInk link to a declaration name.
-/
def declNameToInkLink (name : Name) : HtmlM String := do
let res ← getResult
2022-07-20 14:18:57 +00:00
let module := res.moduleNames[res.name2ModIdx.find! name |>.toNat]!
2022-07-23 11:01:25 +00:00
pure <| (←moduleNameToInkLink module) ++ "#" ++ name.toString
/--
Returns the HTML doc-gen4 link to a declaration name with "break_within"
set as class.
-/
def declNameToHtmlBreakWithinLink (name : Name) : HtmlM Html := do
pure <a class="break_within" href={←declNameToLink name}>{name.toString}</a>
2022-05-19 19:05:17 +00:00
/--
In Lean syntax declarations the following pattern is quite common:
```
syntax term " + " term : term
```
that is, we place spaces around the operator in the middle. When the
`InfoTree` framework provides us with information about what source token
corresponds to which identifier it will thus say that `" + "` corresponds to
`HAdd.hadd`. This is however not the way we want this to be linked, in the HTML
only `+` should be linked, taking care of this is what this function is
responsible for.
-/
def splitWhitespaces (s : String) : (String × String × String) := Id.run do
2022-07-23 11:01:25 +00:00
let front := "".pushn ' ' <| s.offsetOfPos (s.find (!Char.isWhitespace ·))
let mut s := s.trimLeft
let back := "".pushn ' ' (s.length - s.offsetOfPos (s.find Char.isWhitespace))
2022-04-09 17:18:21 +00:00
s := s.trimRight
(front, s, back)
2022-05-19 19:05:17 +00:00
/--
Turns a `CodeWithInfos` object, that is basically a Lean syntax tree with
information about what the identifiers mean, into an HTML object that links
to as much information as possible.
-/
partial def infoFormatToHtml (i : CodeWithInfos) : HtmlM (Array Html) := do
match i with
2022-11-20 12:10:05 +00:00
| .text t => pure #[Html.escape t]
| .append tt => tt.foldlM (λ acc t => do pure <| acc ++ (←infoFormatToHtml t)) #[]
| .tag a t =>
match a.info.val.info with
| Info.ofTermInfo i =>
2022-08-11 21:19:31 +00:00
let cleanExpr := i.expr.consumeMData
2022-11-20 12:10:05 +00:00
match cleanExpr with
| .const name _ =>
2022-08-11 21:19:31 +00:00
-- TODO: this is some very primitive blacklisting but real Blacklisting needs MetaM
-- find a better solution
if (←getResult).name2ModIdx.contains name then
match t with
2022-11-20 12:10:05 +00:00
| .text t =>
2022-08-11 21:19:31 +00:00
let (front, t, back) := splitWhitespaces <| Html.escape t
let elem := <a href={←declNameToLink name}>{t}</a>
pure #[Html.text front, elem, Html.text back]
| _ =>
pure #[<a href={←declNameToLink name}>[←infoFormatToHtml t]</a>]
else
pure #[<span class="fn">[←infoFormatToHtml t]</span>]
2022-11-20 12:10:05 +00:00
| .sort _ =>
match t with
| .text t =>
let mut sortPrefix :: rest := t.splitOn " " | unreachable!
let sortLink := <a href={s!"{← getRoot}foundational_types.html"}>{sortPrefix}</a>
if rest != [] then
rest := " " :: rest
pure #[sortLink, Html.text <| String.join rest]
| _ =>
pure #[<a href={s!"{← getRoot}foundational_types.html"}>[← infoFormatToHtml t]</a>]
| _ =>
pure #[<span class="fn">[←infoFormatToHtml t]</span>]
| _ => pure #[<span class="fn">[←infoFormatToHtml t]</span>]
2022-07-21 21:01:15 +00:00
def baseHtmlHeadDeclarations : BaseHtmlM (Array Html) := do
pure #[
<meta charset="UTF-8"/>,
<meta name="viewport" content="width=device-width, initial-scale=1"/>,
<link rel="stylesheet" href={s!"{←getRoot}style.css"}/>,
<link rel="stylesheet" href={s!"{←getRoot}src/pygments.css"}/>,
2022-07-21 21:01:15 +00:00
<link rel="shortcut icon" href={s!"{←getRoot}favicon.ico"}/>,
<link rel="prefetch" href={s!"{←getRoot}/declarations/declaration-data.bmp"} as="image"/>
2022-07-21 21:01:15 +00:00
]
2022-05-19 19:05:17 +00:00
end DocGen4.Output