From 20e136bb270b39a1d8adc30cbe333124011d0e06 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Thu, 19 May 2022 21:40:22 +0200 Subject: [PATCH] refactor: centralized methods for internal linking infrastructure --- DocGen4/Output/Base.lean | 21 +++++++++++++ DocGen4/Output/Class.lean | 2 +- DocGen4/Output/Module.lean | 61 ++++++++++++++++++++++++++++++-------- DocGen4/Output/Navbar.lean | 4 +-- 4 files changed, 73 insertions(+), 15 deletions(-) diff --git a/DocGen4/Output/Base.lean b/DocGen4/Output/Base.lean index 3cedc79..cdcbca6 100644 --- a/DocGen4/Output/Base.lean +++ b/DocGen4/Output/Base.lean @@ -67,6 +67,12 @@ def moduleNameToLink (n : Name) : HtmlM String := do let parts := n.components.map Name.toString pure $ (← getRoot) ++ (parts.intersperse "/").foldl (· ++ ·) "" ++ ".html" +/-- +Returns the HTML doc-gen4 link to a module name. +-/ +def moduleToHtmlLink (module : Name) : HtmlM Html := do + pure {module.toString} + /-- Returns the path to the HTML file that contains information about a module. -/ @@ -104,6 +110,21 @@ def declNameToLink (name : Name) : HtmlM String := do let module := res.moduleNames[res.name2ModIdx.find! name] pure $ (←moduleNameToLink module) ++ "#" ++ name.toString +/-- +Returns the HTML doc-gen4 link to a declaration name. +-/ +def declNameToHtmlLink (name : Name) : HtmlM Html := do + let link ← declNameToLink name + pure {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 + let link ← declNameToLink name + pure {name.toString} + /-- In Lean syntax declarations the following pattern is quite common: ``` diff --git a/DocGen4/Output/Class.lean b/DocGen4/Output/Class.lean index 00fd252..e39a424 100644 --- a/DocGen4/Output/Class.lean +++ b/DocGen4/Output/Class.lean @@ -8,7 +8,7 @@ open scoped DocGen4.Jsx open Lean def classInstanceToHtml (name : Name) : HtmlM Html := do - pure
  • {name.toString}
    • + pure
  • {←declNameToHtmlLink name}
    • def classInstancesToHtml (instances : Array Name) : HtmlM Html := do let instancesHtml ← instances.mapM classInstanceToHtml diff --git a/DocGen4/Output/Module.lean b/DocGen4/Output/Module.lean index 062a3ca..a9efe14 100644 --- a/DocGen4/Output/Module.lean +++ b/DocGen4/Output/Module.lean @@ -19,6 +19,10 @@ namespace Output open scoped DocGen4.Jsx open Lean +/-- +Render an `Arg` as HTML, adding opacity effects etc. depending on what +type of binder it has. +-/ def argToHtml (arg : Arg) : HtmlM Html := do let (l, r, implicit) := match arg.binderInfo with | BinderInfo.default => ("(", ")", false) @@ -37,19 +41,27 @@ def argToHtml (arg : Arg) : HtmlM Html := do else pure html +/-- +Render the structures this structure extends from as HTML so it can be +added to the top level. +-/ def structureInfoHeader (s : StructureInfo) : HtmlM (Array Html) := do let mut nodes := #[] if s.parents.size > 0 then nodes := nodes.push extends let mut parents := #[] for parent in s.parents do - let link := {parent.toString} + let link ← declNameToHtmlBreakWithinLink parent let inner := Html.element "span" true #[("class", "fn")] #[link] let html:= Html.element "span" false #[("class", "decl_parent")] #[inner] parents := parents.push html nodes := nodes.append (parents.toList.intersperse (Html.text ", ")).toArray pure nodes +/-- +Render the general header of a declaration containing its declaration type +and name. +-/ def docInfoHeader (doc : DocInfo) : HtmlM Html := do let mut nodes := #[] nodes := nodes.push {doc.getKindDescription} @@ -63,7 +75,6 @@ def docInfoHeader (doc : DocInfo) : HtmlM Html := do for arg in doc.getArgs do nodes := nodes.push (←argToHtml arg) - -- TODO: dedup this match doc with | DocInfo.structureInfo i => nodes := nodes.append (←structureInfoHeader i) | DocInfo.classInfo i => nodes := nodes.append (←structureInfoHeader i.toStructureInfo) @@ -73,6 +84,9 @@ def docInfoHeader (doc : DocInfo) : HtmlM Html := do nodes := nodes.push $ Html.element "div" true #[("class", "decl_type")] (←infoFormatToHtml doc.getType) pure
    [nodes]
    +/-- +The main entry point for rendering a single declaration inside a given module. +-/ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do -- basic info like headers, types, structure fields, etc. let docInfoHtml ← match doc with @@ -114,12 +128,20 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do +/-- +Rendering a module doc string, that is the ones with an ! after the opener +as HTML. +-/ def modDocToHtml (module : Name) (mdoc : ModuleDoc) : HtmlM Html := do pure
    [←docStringToHtml mdoc.doc]
    +/-- +Render a module member, that is either a module doc string or a declaration +as HTML. +-/ def moduleMemberToHtml (module : Name) (member : ModuleMember) : HtmlM Html := do match member with | ModuleMember.docInfo d => docInfoToHtml module d @@ -130,10 +152,9 @@ def declarationToNavLink (module : Name) : Html := {module.toString} --- TODO: Similar functions are used all over the place, we should dedup them -def moduleToNavLink (module : Name) : HtmlM Html := do - pure {module.toString} - +/-- +Returns the list of all imports this module does. +-/ def getImports (module : Name) : HtmlM (Array Name) := do let res ← getResult let some idx := res.moduleNames.findIdx? (. == module) | unreachable! @@ -144,6 +165,17 @@ def getImports (module : Name) : HtmlM (Array Name) := do imports := imports.push (res.moduleNames.get! i) pure imports +/-- +Sort the list of all modules this one is importing, linkify it +and return the HTML. +-/ +def importsHtml (moduleName : Name) : HtmlM (Array Html) := do + let imports := (←getImports moduleName) |>.qsort Name.lt + imports.mapM (λ i => do pure
  • {←moduleToHtmlLink i}
    • ) + +/-- +Returns a list of all modules this module is imported by. +-/ def getImportedBy (module : Name) : HtmlM (Array Name) := do let res ← getResult let some idx := res.moduleNames.findIdx? (. == module) | unreachable! @@ -154,15 +186,17 @@ def getImportedBy (module : Name) : HtmlM (Array Name) := do impBy := impBy.push (res.moduleNames.get! i) pure impBy +/-- +Sort the list of all modules this one is imported by, linkify it +and return the HTML. +-/ def importedByHtml (moduleName : Name) : HtmlM (Array Html) := do let imports := (←getImportedBy moduleName) |>.qsort Name.lt - imports.mapM (λ i => do pure
  • {←moduleToNavLink i}
    • ) - - -def importsHtml (moduleName : Name) : HtmlM (Array Html) := do - let imports := (←getImports moduleName) |>.qsort Name.lt - imports.mapM (λ i => do pure
  • {←moduleToNavLink i}
    • ) + imports.mapM (λ i => do pure
  • {←moduleToHtmlLink i}
    • ) +/-- +Render the internal nav bar (the thing on the right on all module pages). +-/ def internalNav (members : Array Name) (moduleName : Name) : HtmlM Html := do pure +/-- +The main entry point to rendering the HTML for an entire module. +-/ def moduleToHtml (module : Module) : HtmlM Html := withReader (setCurrentName module.name) do let memberDocs ← module.members.mapM (λ i => moduleMemberToHtml module.name i) let memberNames := filterMapDocInfo module.members |>.map DocInfo.getName diff --git a/DocGen4/Output/Navbar.lean b/DocGen4/Output/Navbar.lean index c9cb196..3db6033 100644 --- a/DocGen4/Output/Navbar.lean +++ b/DocGen4/Output/Navbar.lean @@ -15,7 +15,7 @@ open scoped DocGen4.Jsx def moduleListFile (file : Name) : HtmlM Html := do pure
    - {file.toString} + {←moduleToHtmlLink file}
    partial def moduleListDir (h : Hierarchy) : HtmlM Html := do @@ -31,7 +31,7 @@ partial def moduleListDir (h : Hierarchy) : HtmlM Html := do [if (←getCurrentName).any (h.getName.isPrefixOf ·) then #[("open", "")] else #[]]> { if (←getResult).moduleInfo.contains h.getName then - Html.element "summary" true #[] #[{h.getName.toString}] + Html.element "summary" true #[] #[←moduleToHtmlLink h.getName] else {h.getName.toString} }