r
/
bookshelf-doc
mirror of https://github.com/jrpotter/bookshelf-doc
1
Fork 0
Code Issues Packages Projects Releases Wiki Activity

refactor: use `rawIdent`

main
Sebastian Ullrich 2022-05-19 11:14:47 +02:00
parent fc48deaf81
commit 41f6eb0835
7 changed files with 47 additions and 47 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
DocGen4/Output/Definition.lean
View File

@ -11,7 +11,7 @@ open Lean Widget
def equationLimit : Nat := 200
def equationToHtml (c : CodeWithInfos) : HtmlM Html := do
pure <li «class»="equation">[←infoFormatToHtml c]</li>
pure <li class="equation">[←infoFormatToHtml c]</li>
def equationsToHtml (i : DefinitionInfo) : HtmlM (Array Html) := do
if let some eqs := i.equations then
@ -21,8 +21,8 @@ def equationsToHtml (i : DefinitionInfo) : HtmlM (Array Html) := do
pure #[
<details>
<summary>Equations</summary>
<ul «class»="equations">
<li «class»="equation">One or more equations did not get rendered due to their size.</li>
<ul class="equations">
<li class="equation">One or more equations did not get rendered due to their size.</li>
[filteredEquationsHtml]
</ul>
</details>
@ -31,7 +31,7 @@ def equationsToHtml (i : DefinitionInfo) : HtmlM (Array Html) := do
pure #[
<details>
<summary>Equations</summary>
<ul «class»="equations">
<ul class="equations">
[filteredEquationsHtml]
</ul>
</details>

2
DocGen4/Output/Inductive.lean
View File

@ -9,7 +9,7 @@ open scoped DocGen4.Jsx
def ctorToHtml (i : NameInfo) : HtmlM Html := do
let shortName := i.name.components'.head!.toString
let name := i.name.toString
pure <li «class»="constructor" id={name}>{shortName} : [←infoFormatToHtml i.type]</li>
pure <li class="constructor" id={name}>{shortName} : [←infoFormatToHtml i.type]</li>
def inductiveToHtml (i : InductiveInfo) : HtmlM (Array Html) := do
let constructorsHtml := <ul "class"="constructors">[← i.ctors.toArray.mapM ctorToHtml]</ul>

36
DocGen4/Output/Module.lean
View File

@ -33,17 +33,17 @@ def argToHtml (arg : Arg) : HtmlM Html := do
let inner := Html.element "span" true #[("class", "fn")] nodes
let html := Html.element "span" false #[("class", "decl_args")] #[inner]
if implicit then
pure <span «class»="impl_arg">{html}</span>
pure <span class="impl_arg">{html}</span>
else
pure html
def structureInfoHeader (s : StructureInfo) : HtmlM (Array Html) := do
let mut nodes := #[]
if s.parents.size > 0 then
nodes := nodes.push <span «class»="decl_extends">extends</span>
nodes := nodes.push <span class="decl_extends">extends</span>
let mut parents := #[]
for parent in s.parents do
let link := <a «class»="break_within" href={←declNameToLink parent}>{parent.toString}</a>
let link := <a class="break_within" href={←declNameToLink parent}>{parent.toString}</a>
let inner := Html.element "span" true #[("class", "fn")] #[link]
let html:= Html.element "span" false #[("class", "decl_parent")] #[inner]
parents := parents.push html
@ -52,10 +52,10 @@ def structureInfoHeader (s : StructureInfo) : HtmlM (Array Html) := do
def docInfoHeader (doc : DocInfo) : HtmlM Html := do
let mut nodes := #[]
nodes := nodes.push <span «class»="decl_kind">{doc.getKindDescription}</span>
nodes := nodes.push <span class="decl_kind">{doc.getKindDescription}</span>
nodes := nodes.push
<span «class»="decl_name">
<a «class»="break_within" href={←declNameToLink doc.getName}>
<span class="decl_name">
<a class="break_within" href={←declNameToLink doc.getName}>
-- TODO: HTMLify the name
{doc.getName.toString}
</a>
@ -69,9 +69,9 @@ def docInfoHeader (doc : DocInfo) : HtmlM Html := do
| DocInfo.classInfo i => nodes := nodes.append (←structureInfoHeader i.toStructureInfo)
| _ => nodes := nodes
nodes := nodes.push <span «class»="decl_args">:</span>
nodes := nodes.push <span class="decl_args">:</span>
nodes := nodes.push $ Html.element "div" true #[("class", "decl_type")] (←infoFormatToHtml doc.getType)
pure <div «class»="decl_header"> [nodes] </div>
pure <div class="decl_header"> [nodes] </div>
def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
-- basic info like headers, types, structure fields, etc.
@ -101,9 +101,9 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
#[]
pure
<div «class»="decl" id={doc.getName.toString}>
<div «class»={doc.getKind}>
<div «class»="gh_link">
<div class="decl" id={doc.getName.toString}>
<div class={doc.getKind}>
<div class="gh_link">
<a href={←getSourceUrl module doc.getDeclarationRange}>source</a>
</div>
[attrsHtml]
@ -116,7 +116,7 @@ def docInfoToHtml (module : Name) (doc : DocInfo) : HtmlM Html := do
def modDocToHtml (module : Name) (mdoc : ModuleDoc) : HtmlM Html := do
pure
<div «class»="mod_doc">
<div class="mod_doc">
[←docStringToHtml mdoc.doc]
</div>
@ -126,8 +126,8 @@ def moduleMemberToHtml (module : Name) (member : ModuleMember) : HtmlM Html := d
| ModuleMember.modDoc d => modDocToHtml module d
def declarationToNavLink (module : Name) : Html :=
<div «class»="nav_link">
<a «class»="break_within" href={s!"#{module.toString}"}>{module.toString}</a>
<div class="nav_link">
<a class="break_within" href={s!"#{module.toString}"}>{module.toString}</a>
</div>
-- TODO: Similar functions are used all over the place, we should dedup them
@ -165,10 +165,10 @@ def importsHtml (moduleName : Name) : HtmlM (Array Html) := do
def internalNav (members : Array Name) (moduleName : Name) : HtmlM Html := do
pure
<nav «class»="internal_nav">
<h3><a «class»="break_within" href="#top">{moduleName.toString}</a></h3>
<p «class»="gh_nav_link"><a href={←getSourceUrl moduleName none}>source</a></p>
<div «class»="imports">
<nav class="internal_nav">
<h3><a class="break_within" href="#top">{moduleName.toString}</a></h3>
<p class="gh_nav_link"><a href={←getSourceUrl moduleName none}>source</a></p>
<div class="imports">
<details>
<summary>Imports</summary>
<ul>

18
DocGen4/Output/Navbar.lean
View File

@ -14,7 +14,7 @@ open Lean
open scoped DocGen4.Jsx
def moduleListFile (file : Name) : HtmlM Html := do
pure <div «class»={if (← getCurrentName) == file then "nav_link visible" else "nav_link"}>
pure <div class={if (← getCurrentName) == file then "nav_link visible" else "nav_link"}>
<a href={← moduleNameToLink file}>{file.toString}</a>
</div>
@ -48,17 +48,17 @@ def moduleList : HtmlM Html := do
def navbar : HtmlM Html := do
pure
<nav «class»="nav">
<nav class="nav">
<h3>General documentation</h3>
<div «class»="nav_link"><a href={s!"{←getRoot}"}>index</a></div>
<div class="nav_link"><a href={s!"{←getRoot}"}>index</a></div>
/-
TODO: Add these in later
<div «class»="nav_link"><a href={s!"{←getRoot}tactics.html"}>tactics</a></div>
<div «class»="nav_link"><a href={s!"{←getRoot}commands.html"}>commands</a></div>
<div «class»="nav_link"><a href={s!"{←getRoot}hole_commands.html"}>hole commands</a></div>
<div «class»="nav_link"><a href={s!"{←getRoot}attributes.html"}>attributes</a></div>
<div «class»="nav_link"><a href={s!"{←getRoot}notes.html"}>notes</a></div>
<div «class»="nav_link"><a href={s!"{←getRoot}references.html"}>references</a></div>
<div class="nav_link"><a href={s!"{←getRoot}tactics.html"}>tactics</a></div>
<div class="nav_link"><a href={s!"{←getRoot}commands.html"}>commands</a></div>
<div class="nav_link"><a href={s!"{←getRoot}hole_commands.html"}>hole commands</a></div>
<div class="nav_link"><a href={s!"{←getRoot}attributes.html"}>attributes</a></div>
<div class="nav_link"><a href={s!"{←getRoot}notes.html"}>notes</a></div>
<div class="nav_link"><a href={s!"{←getRoot}references.html"}>references</a></div>
-/
<h3>Library</h3>
{← moduleList}

20
DocGen4/Output/Structure.lean
View File

@ -13,30 +13,30 @@ def fieldToHtml (f : NameInfo) : HtmlM Html := do
if let some doc := f.doc then
let renderedDoc ← docStringToHtml doc
pure
<li id={name} «class»="structure_field">
<div «class»="structure_field_doc">[renderedDoc]</div>
<div «class»="structure_field_info">{s!"{shortName} "} : [←infoFormatToHtml f.type]</div>
<li id={name} class="structure_field">
<div class="structure_field_doc">[renderedDoc]</div>
<div class="structure_field_info">{s!"{shortName} "} : [←infoFormatToHtml f.type]</div>
</li>
else
pure
<li id={name} «class»="structure_field">
<div «class»="structure_field_info">{s!"{shortName} "} : [←infoFormatToHtml f.type]</div>
<li id={name} class="structure_field">
<div class="structure_field_info">{s!"{shortName} "} : [←infoFormatToHtml f.type]</div>
</li>
def structureToHtml (i : StructureInfo) : HtmlM (Array Html) := do
let structureHtml :=
if Name.isSuffixOf `mk i.ctor.name then
(<ul «class»="structure_fields" id={i.ctor.name.toString}>
(<ul class="structure_fields" id={i.ctor.name.toString}>
[←i.fieldInfo.mapM fieldToHtml]
</ul>)
else
let ctorShortName := i.ctor.name.components'.head!.toString
(<ul «class»="structure_ext">
<li id={i.ctor.name.toString} «class»="structure_ext_ctor">{s!"{ctorShortName} "} :: (</li>
<ul «class»="structure_ext_fields">
(<ul class="structure_ext">
<li id={i.ctor.name.toString} class="structure_ext_ctor">{s!"{ctorShortName} "} :: (</li>
<ul class="structure_ext_fields">
[←i.fieldInfo.mapM fieldToHtml]
</ul>
<li «class»="structure_ext_ctor">)</li>
<li class="structure_ext_ctor">)</li>
</ul>)
pure #[structureHtml]

4
DocGen4/Output/Template.lean
View File

@ -42,8 +42,8 @@ def baseHtmlArray (title : String) (site : Array Html) : HtmlM Html := do
<input id="nav_toggle" type="checkbox"/>
<header>
<h1><label «for»="nav_toggle"></label>Documentation</h1>
<p «class»="header_filename break_within">{title}</p>
<h1><label for="nav_toggle"></label>Documentation</h1>
<p class="header_filename break_within">{title}</p>
-- TODO: Replace this form with our own search
<form action="https://google.com/search" method="get" id="search_form">
<input type="hidden" name="sitesearch" value="https://leanprover-community.github.io/mathlib_docs"/>

6
DocGen4/ToHtmlFormat.lean
View File

@ -81,14 +81,14 @@ def jsxText : Parser :=
@[combinatorFormatter DocGen4.Jsx.jsxText] def jsxText.formatter : Formatter := pure ()
@[combinatorParenthesizer DocGen4.Jsx.jsxText] def jsxText.parenthesizer : Parenthesizer := pure ()
syntax jsxAttrName := ident <|> str
syntax jsxAttrName := rawIdent <|> str
syntax jsxAttrVal := str <|> group("{" term "}")
syntax jsxSimpleAttr := jsxAttrName "=" jsxAttrVal
syntax jsxAttrSpread := "[" term "]"
syntax jsxAttr := jsxSimpleAttr <|> jsxAttrSpread
syntax "<" ident jsxAttr* "/>" : jsxElement
syntax "<" ident jsxAttr* ">" jsxChild* "</" ident ">" : jsxElement
syntax "<" rawIdent jsxAttr* "/>" : jsxElement
syntax "<" rawIdent jsxAttr* ">" jsxChild* "</" rawIdent ">" : jsxElement
syntax jsxText : jsxChild
syntax "{" term "}" : jsxChild