/- 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 import DocGen4.Output.ToHtmlFormat namespace DocGen4.Output open scoped DocGen4.Jsx open Lean System Widget Elab Process def basePath := FilePath.mk "." / "build" / "doc" def srcBasePath := basePath / "src" def declarationsBasePath := basePath / "declarations" /-- The context used in the `BaseHtmlM` monad for HTML templating. -/ structure SiteBaseContext where /-- The module hierarchy as a tree structure. -/ hierarchy : Hierarchy /-- How far away we are from the page root, used for relative links to the root. -/ 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 /-- The Github URL of the project that we are building docs for. -/ projectGithubUrl : String /-- The commit of the project that we are building docs for. -/ projectCommit : String /-- The context used in the `HtmlM` monad for HTML templating. -/ structure SiteContext where /-- The full analysis result from the Process module. -/ result : AnalyzerResult /-- A function to link declaration names to their source URLs, usually Github ones. -/ 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 return x.run (← readThe SiteContext) (← readThe SiteBaseContext) instance [Monad m] : MonadLift BaseHtmlM (BaseHtmlT m) where monadLift x := do return x.run (← readThe SiteBaseContext) /-- 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 return (← read).hierarchy def getCurrentName : BaseHtmlM (Option Name) := do return (← read).currentName def getResult : HtmlM AnalyzerResult := do return (← read).result def getSourceUrl (module : Name) (range : Option DeclarationRange): HtmlM String := do return (← read).sourceLinker module range def leanInkEnabled? : HtmlM Bool := do return (← read).leanInkEnabled def getProjectGithubUrl : BaseHtmlM String := do return (← read).projectGithubUrl def getProjectCommit : BaseHtmlM String := do return (← read).projectCommit /-- 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. -/ 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) /- Returns the doc-gen4 link to a module `NameExt`. -/ def moduleNameExtToLink (n : NameExt) : BaseHtmlM String := do let parts := n.name.components.map Name.toString return (← getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ "." ++ n.ext.toString /-- Returns the doc-gen4 link to a module name. -/ def moduleNameToHtmlLink (n : Name) : BaseHtmlM String := moduleNameExtToLink ⟨n, .html⟩ /-- Returns the HTML doc-gen4 link to a module name. -/ def moduleToHtmlLink (module : Name) : BaseHtmlM Html := do return {module.toString} /-- Returns the LeanInk link to a module name. -/ def moduleNameToInkLink (n : Name) : BaseHtmlM String := do let parts := "src" :: n.components.map Name.toString return (← 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 := let parts := n.components.map Name.toString 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 := let parts := n.components.dropLast.map Name.toString basePath / parts.foldl (· / ·) (FilePath.mk ".") 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 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" 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" 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 /-- Returns the doc-gen4 link to a declaration name. -/ def declNameToLink (name : Name) : HtmlM String := do let res ← getResult let module := res.moduleNames[res.name2ModIdx.find! name |>.toNat]! return (← moduleNameToHtmlLink module) ++ "#" ++ name.toString /-- Returns the HTML doc-gen4 link to a declaration name. -/ def declNameToHtmlLink (name : Name) : HtmlM Html := do return {name.toString} /-- Returns the LeanInk link to a declaration name. -/ def declNameToInkLink (name : Name) : HtmlM String := do let res ← getResult let module := res.moduleNames[res.name2ModIdx.find! name |>.toNat]! return (← moduleNameToInkLink module) ++ "#" ++ name.toString /-- Returns a name splitted into parts. Together with "break_within" CSS class this helps browser to break a name nicely. -/ def breakWithin (name: String) : (Array Html) := name.splitOn "." |> .map (fun (s: String) => {s}) |> .intersperse "." |> List.toArray /-- Returns the HTML doc-gen4 link to a declaration name with "break_within" set as class. -/ def declNameToHtmlBreakWithinLink (name : Name) : HtmlM Html := do return [breakWithin 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 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)) s := s.trimRight (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 match i with | .text t => return #[Html.escape t] | .append tt => tt.foldlM (fun acc t => do return acc ++ (← infoFormatToHtml t)) #[] | .tag a t => match a.info.val.info with | Info.ofTermInfo i => let cleanExpr := i.expr.consumeMData match cleanExpr with | .const name _ => -- 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 | .text t => let (front, t, back) := splitWhitespaces <| Html.escape t let elem := {t} return #[Html.text front, elem, Html.text back] | _ => return #[[← infoFormatToHtml t]] else return #[[← infoFormatToHtml t]] | .sort _ => match t with | .text t => let mut sortPrefix :: rest := t.splitOn " " | unreachable! let sortLink := {sortPrefix} if rest != [] then rest := " " :: rest return #[sortLink, Html.text <| String.join rest] | _ => return #[[← infoFormatToHtml t]] | _ => return #[[← infoFormatToHtml t]] | _ => return #[[← infoFormatToHtml t]] def baseHtmlHeadDeclarations : BaseHtmlM (Array Html) := do return #[ , , , , , ] end DocGen4.Output