bookshelf-doc/DocGen4/Output/ToHtmlFormat.lean

148 lines
5.0 KiB
Plaintext
Raw Normal View History

/-
Copyright (c) 2021 Wojciech Nawrocki. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Wojciech Nawrocki, Sebastian Ullrich, Henrik Böving
-/
import Lean.Data.Json
import Lean.Parser
/-! This module defines:
- a representation of HTML trees
- together with a JSX-like DSL for writing them
- and widget support for visualizing any type as HTML. -/
namespace DocGen4
open Lean
inductive Html where
-- TODO(WN): it's nameless for shorter JSON; re-add names when we have deriving strategies for From/ToJson
-- element (tag : String) (flatten : Bool) (attrs : Array HtmlAttribute) (children : Array Html)
| element : String → Bool → Array (String × String) → Array Html → Html
| text : String → Html
deriving Repr, BEq, Inhabited, FromJson, ToJson
instance : Coe String Html :=
⟨Html.text⟩
namespace Html
def attributesToString (attrs : Array (String × String)) :String :=
attrs.foldl (λ acc (k, v) => acc ++ " " ++ k ++ "=\"" ++ v ++ "\"") ""
-- TODO: Termination proof
partial def toStringAux : Html → String
| element tag false attrs #[text s] => s!"<{tag}{attributesToString attrs}>{s}</{tag}>\n"
| element tag false attrs #[child] => s!"<{tag}{attributesToString attrs}>\n{child.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
def toString (html : Html) : String :=
html.toStringAux.trimRight
instance : ToString Html :=
⟨toString⟩
partial def textLength : Html → Nat
| text s => s.length
| element _ _ _ children =>
let lengths := children.map textLength
lengths.foldl Nat.add 0
def escapePairs : Array (String × String) :=
#[
("&", "&amp"),
("<", "&lt"),
(">", "&gt"),
("\"", "&quot")
]
def escape (s : String) : String :=
escapePairs.foldl (λ acc (o, r) => acc.replace o r) s
end Html
namespace Jsx
open Parser PrettyPrinter
declare_syntax_cat jsxElement
declare_syntax_cat jsxChild
-- JSXTextCharacter : SourceCharacter but not one of {, <, > or }
def jsxText : Parser :=
withAntiquot (mkAntiquot "jsxText" `jsxText) {
fn := fun c s =>
let startPos := s.pos
let s := takeWhile1Fn (not ∘ "[{<>}]$".contains) "expected JSX text" c s
mkNodeToken `jsxText startPos c s }
@[combinatorFormatter DocGen4.Jsx.jsxText] def jsxText.formatter : Formatter := pure ()
@[combinatorParenthesizer DocGen4.Jsx.jsxText] def jsxText.parenthesizer : Parenthesizer := pure ()
2022-05-19 09:14:47 +00:00
syntax jsxAttrName := rawIdent <|> str
2022-04-09 17:18:21 +00:00
syntax jsxAttrVal := str <|> group("{" term "}")
2022-01-20 13:49:50 +00:00
syntax jsxSimpleAttr := jsxAttrName "=" jsxAttrVal
syntax jsxAttrSpread := "[" term "]"
syntax jsxAttr := jsxSimpleAttr <|> jsxAttrSpread
2022-05-19 09:14:47 +00:00
syntax "<" rawIdent jsxAttr* "/>" : jsxElement
syntax "<" rawIdent jsxAttr* ">" jsxChild* "</" rawIdent ">" : jsxElement
2022-01-20 13:49:50 +00:00
syntax jsxText : jsxChild
syntax "{" term "}" : jsxChild
syntax "[" term "]" : jsxChild
syntax jsxElement : jsxChild
scoped syntax:max jsxElement : term
2022-01-20 13:49:50 +00:00
def translateAttrs (attrs : Array Syntax) : MacroM Syntax := do
let mut as ← `(#[])
for attr in attrs do
as ← match attr with
| `(jsxAttr| $n:jsxAttrName=$v:jsxAttrVal) =>
let n ← match n with
2022-04-09 17:18:21 +00:00
| `(jsxAttrName| $n:str) => pure n
2022-02-09 21:45:28 +00:00
| `(jsxAttrName| $n:ident) => pure $ quote (toString n.getId)
2022-01-20 13:49:50 +00:00
| _ => Macro.throwUnsupported
let v ← match v with
2022-02-09 21:45:28 +00:00
| `(jsxAttrVal| {$v}) => pure v
2022-04-09 17:18:21 +00:00
| `(jsxAttrVal| $v:str) => pure v
2022-01-20 13:49:50 +00:00
| _ => Macro.throwUnsupported
2022-01-20 13:51:24 +00:00
`(($as).push ($n, ($v : String)))
2022-01-20 13:49:50 +00:00
| `(jsxAttr| [$t]) => `($as ++ ($t : Array (String × String)))
| _ => Macro.throwUnsupported
return as
2022-06-20 16:39:55 +00:00
private def htmlHelper (n : Syntax) (children : Array Syntax) (m : Syntax) : MacroM (String × Syntax):= do
unless n.getId == m.getId do
withRef m <| Macro.throwError s!"Leading and trailing part of tags don't match: '{n}', '{m}'"
let mut cs ← `(#[])
for child in children do
cs ← match child with
| `(jsxChild|$t:jsxText) => `(($cs).push (Html.text $(quote t[0].getAtomVal!)))
-- TODO(WN): elab as list of children if type is `t Html` where `Foldable t`
| `(jsxChild|{$t}) => `(($cs).push ($t : Html))
| `(jsxChild|[$t]) => `($cs ++ ($t : Array Html))
| `(jsxChild|$e:jsxElement) => `(($cs).push ($e:jsxElement : Html))
| _ => Macro.throwUnsupported
let tag := toString n.getId
pure $ (tag, cs)
macro_rules
2022-01-20 13:49:50 +00:00
| `(<$n $attrs* />) => do
`(Html.element $(quote (toString n.getId)) true $(← translateAttrs attrs) #[])
| `(<$n $attrs* >$children*</$m>) => do
2022-06-20 16:39:55 +00:00
let (tag, children) ← htmlHelper n children m
`(Html.element $(quote tag) true $(← translateAttrs attrs) $children)
end Jsx
/-- A type which implements `ToHtmlFormat` will be visualized
as the resulting HTML in editors which support it. -/
class ToHtmlFormat (α : Type u) where
formatHtml : α → Html
end DocGen4