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

feat: Newline free HTML formatting 

Some of the HTML elements we are generating are newline sensitive
which requires the HTML to String formatter to optionally omit
additional newlines.
main
Henrik Böving 2021-12-25 14:04:35 +01:00
parent d18e71966c
commit 0efbcd1f60
2 changed files with 10 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
DocGen4/Output/Navbar.lean
View File

@ -22,7 +22,7 @@ def moduleListFile (file : Name) : HtmlM Html := do
#[("class", "nav_link")] #[("class", "nav_link")]
| none => #[("class", "nav_link")] | none => #[("class", "nav_link")]
let nodes := #[<a href={s!"{←moduleNameToLink file}"}>{file.toString}</a>] let nodes := #[<a href={s!"{←moduleNameToLink file}"}>{file.toString}</a>]
return Html.element "div" attributes nodes return Html.element "div" false attributes nodes
partial def moduleListDir (h : Hierarchy) : HtmlM Html := do partial def moduleListDir (h : Hierarchy) : HtmlM Html := do
let children := Array.mk (h.getChildren.toList.map Prod.snd) let children := Array.mk (h.getChildren.toList.map Prod.snd)
@ -40,7 +40,7 @@ partial def moduleListDir (h : Hierarchy) : HtmlM Html := do
| none => | none =>
#[("class", "nav_sect"), ("data-path", moduleLink)] #[("class", "nav_sect"), ("data-path", moduleLink)]
let nodes := #[<summary>{h.getName.toString}</summary>] ++ dirNodes ++ fileNodes let nodes := #[<summary>{h.getName.toString}</summary>] ++ dirNodes ++ fileNodes
return Html.element "details" attributes nodes return Html.element "details" false attributes nodes
def moduleList : HtmlM (Array Html) := do def moduleList : HtmlM (Array Html) := do
let hierarchy := (←getResult).hierarchy let hierarchy := (←getResult).hierarchy

15
DocGen4/ToHtmlFormat.lean
View File

@ -18,8 +18,8 @@ open Lean
inductive Html where inductive Html where
-- TODO(WN): it's nameless for shorter JSON; re-add names when we have deriving strategies for From/ToJson -- TODO(WN): it's nameless for shorter JSON; re-add names when we have deriving strategies for From/ToJson
-- element (tag : String) (attrs : Array HtmlAttribute) (children : Array Html) -- element (tag : String) (flatten : Bool) (attrs : Array HtmlAttribute) (children : Array Html)
| element : String → Array (String × String) → Array Html → Html | element : String → Bool → Array (String × String) → Array Html → Html
| text : String → Html | text : String → Html
deriving Repr, BEq, Inhabited, FromJson, ToJson deriving Repr, BEq, Inhabited, FromJson, ToJson
@ -33,9 +33,10 @@ def attributesToString (attrs : Array (String × String)) :String :=
-- TODO: Termination proof -- TODO: Termination proof
partial def toStringAux : Html → String partial def toStringAux : Html → String
| element tag attrs #[text s] => s!"<{tag}{attributesToString attrs}>{s}</{tag}>\n" | element tag false attrs #[text s] => s!"<{tag}{attributesToString attrs}>{s}</{tag}>\n"
| element tag attrs #[child] => s!"<{tag}{attributesToString attrs}>\n{child.toStringAux}</{tag}>\n" | element tag false attrs #[child] => s!"<{tag}{attributesToString attrs}>\n{child.toStringAux}</{tag}>\n"
| element tag attrs children => s!"<{tag}{attributesToString attrs}>\n{children.foldl (· ++ toStringAux ·) ""}</{tag}>\n" | element tag false attrs children => s!"<{tag}{attributesToString attrs}>\n{children.foldl (· ++ toStringAux ·) ""}</{tag}>\n"
| element tag true attrs children => s!"<{tag}{attributesToString attrs}>{children.foldl (· ++ toStringAux ·) ""}</{tag}>"
| text s => s | text s => s
def toString (html : Html) : String := def toString (html : Html) : String :=
@ -83,7 +84,7 @@ macro_rules
| `(jsxAttrVal| $s:strLit) => s | `(jsxAttrVal| $s:strLit) => s
| `(jsxAttrVal| { $t:term }) => t | `(jsxAttrVal| { $t:term }) => t
| _ => unreachable! | _ => unreachable!
`(Html.element $(quote <| toString n.getId) #[ $[($ns, $vs)],* ] #[]) `(Html.element $(quote <| toString n.getId) false #[ $[($ns, $vs)],* ] #[])
| `(<$n $[$ns = $vs]* >$cs*</$m>) => | `(<$n $[$ns = $vs]* >$cs*</$m>) =>
if n.getId == m.getId then do if n.getId == m.getId then do
let ns := ns.map (quote <| toString ·.getId) let ns := ns.map (quote <| toString ·.getId)
@ -99,7 +100,7 @@ macro_rules
| `(jsxChild|$e:jsxElement) => `(#[$e:jsxElement]) | `(jsxChild|$e:jsxElement) => `(#[$e:jsxElement])
| _ => unreachable! | _ => unreachable!
let tag := toString n.getId let tag := toString n.getId
`(Html.element $(quote tag) #[ $[($ns, $vs)],* ] (Array.foldl Array.append #[] #[ $[$cs],* ])) `(Html.element $(quote tag) false #[ $[($ns, $vs)],* ] (Array.foldl Array.append #[] #[ $[$cs],* ]))
else Macro.throwError ("expected </" ++ toString n.getId ++ ">") else Macro.throwError ("expected </" ++ toString n.getId ++ ">")
end Jsx end Jsx