doc: Output.Base

main
Henrik Böving 2022-05-19 21:05:17 +02:00
parent 0b8f7a1397
commit bdd4a5f612
1 changed files with 59 additions and 4 deletions

View File

@ -7,16 +7,31 @@ import DocGen4.Process
import DocGen4.IncludeStr import DocGen4.IncludeStr
import DocGen4.Output.ToHtmlFormat import DocGen4.Output.ToHtmlFormat
namespace DocGen4 namespace DocGen4.Output
namespace Output
open scoped DocGen4.Jsx open scoped DocGen4.Jsx
open Lean System Widget Elab open Lean System Widget Elab
/--
The context used in the `HtmlM` monad for HTML templating.
-/
structure SiteContext where structure SiteContext where
/--
The full analysis result from the Process module.
-/
result : AnalyzerResult result : AnalyzerResult
/--
How far away we are from the page root, used for relative links to the root.
-/
depthToRoot: Nat depthToRoot: Nat
/--
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 currentName : Option Name
/--
A function to link declaration names to their source URLs, usually Github ones.
-/
sourceLinker : Name → Option DeclarationRange → String sourceLinker : Name → Option DeclarationRange → String
def setCurrentName (name : Name) (ctx : SiteContext) := {ctx with currentName := some name} def setCurrentName (name : Name) (ctx : SiteContext) := {ctx with currentName := some name}
@ -24,6 +39,9 @@ def setCurrentName (name : Name) (ctx : SiteContext) := {ctx with currentName :=
abbrev HtmlT := ReaderT SiteContext abbrev HtmlT := ReaderT SiteContext
abbrev HtmlM := HtmlT Id abbrev HtmlM := HtmlT Id
/--
Obtains the root URL as a relative one to the current depth.
-/
def getRoot : HtmlM String := do def getRoot : HtmlM String := do
let rec go: Nat -> String let rec go: Nat -> String
| 0 => "./" | 0 => "./"
@ -35,22 +53,40 @@ def getResult : HtmlM AnalyzerResult := do pure (←read).result
def getCurrentName : HtmlM (Option Name) := do pure (←read).currentName def getCurrentName : HtmlM (Option Name) := do pure (←read).currentName
def getSourceUrl (module : Name) (range : Option DeclarationRange): HtmlM String := do pure $ (←read).sourceLinker module range def getSourceUrl (module : Name) (range : Option DeclarationRange): HtmlM String := do pure $ (←read).sourceLinker module range
/--
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.
-/
def templateExtends {α β : Type} (base : α → HtmlM β) (new : HtmlM α) : HtmlM β := def templateExtends {α β : Type} (base : α → HtmlM β) (new : HtmlM α) : HtmlM β :=
new >>= base new >>= base
/--
Returns the doc-gen4 link to a module name.
-/
def moduleNameToLink (n : Name) : HtmlM String := do def moduleNameToLink (n : Name) : HtmlM String := do
let parts := n.components.map Name.toString let parts := n.components.map Name.toString
pure $ (← getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html" pure $ (← getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html"
/--
Returns the path to the HTML file that contains information about a module.
-/
def moduleNameToFile (basePath : FilePath) (n : Name) : FilePath := def moduleNameToFile (basePath : FilePath) (n : Name) : FilePath :=
let parts := n.components.map Name.toString let parts := n.components.map Name.toString
FilePath.withExtension (basePath / parts.foldl (· / ·) (FilePath.mk ".")) "html" FilePath.withExtension (basePath / parts.foldl (· / ·) (FilePath.mk ".")) "html"
/--
Returns the directory of the HTML file that contains information about a module.
-/
def moduleNameToDirectory (basePath : FilePath) (n : Name) : FilePath := def moduleNameToDirectory (basePath : FilePath) (n : Name) : FilePath :=
let parts := n.components.dropLast.map Name.toString let parts := n.components.dropLast.map Name.toString
basePath / parts.foldl (· / ·) (FilePath.mk ".") basePath / parts.foldl (· / ·) (FilePath.mk ".")
section Static section Static
/-!
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 styleCss : String := include_str "../../static/style.css"
def declarationDataCenterJs : String := include_str "../../static/declaration-data.js" def declarationDataCenterJs : String := include_str "../../static/declaration-data.js"
def navJs : String := include_str "../../static/nav.js" def navJs : String := include_str "../../static/nav.js"
@ -60,11 +96,26 @@ section Static
def mathjaxConfigJs : String := include_str "../../static/mathjax-config.js" def mathjaxConfigJs : String := include_str "../../static/mathjax-config.js"
end Static end Static
/--
Returns the doc-gen4 link to a declaration name.
-/
def declNameToLink (name : Name) : HtmlM String := do def declNameToLink (name : Name) : HtmlM String := do
let res ← getResult let res ← getResult
let module := res.moduleNames[res.name2ModIdx.find! name] let module := res.moduleNames[res.name2ModIdx.find! name]
pure $ (←moduleNameToLink module) ++ "#" ++ name.toString pure $ (←moduleNameToLink module) ++ "#" ++ name.toString
/--
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 def splitWhitespaces (s : String) : (String × String × String) := Id.run do
let front := "".pushn ' ' $ s.offsetOfPos (s.find (!Char.isWhitespace ·)) let front := "".pushn ' ' $ s.offsetOfPos (s.find (!Char.isWhitespace ·))
let mut s := s.trimLeft let mut s := s.trimLeft
@ -72,6 +123,11 @@ def splitWhitespaces (s : String) : (String × String × String) := Id.run do
s := s.trimRight s := s.trimRight
(front, s, back) (front, s, back)
/--
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 partial def infoFormatToHtml (i : CodeWithInfos) : HtmlM (Array Html) := do
match i with match i with
| TaggedText.text t => pure #[Html.escape t] | TaggedText.text t => pure #[Html.escape t]
@ -93,5 +149,4 @@ partial def infoFormatToHtml (i : CodeWithInfos) : HtmlM (Array Html) := do
pure #[Html.element "span" true #[("class", "fn")] (←infoFormatToHtml t)] pure #[Html.element "span" true #[("class", "fn")] (←infoFormatToHtml t)]
| _ => pure #[Html.element "span" true #[("class", "fn")] (←infoFormatToHtml t)] | _ => pure #[Html.element "span" true #[("class", "fn")] (←infoFormatToHtml t)]
end Output end DocGen4.Output
end DocGen4