@Patrick Massot what would you like to use it for? We have it here https://github.com/EdAyers/WidgetKit/blob/main/WidgetKit/Html.lean , but there it will be specialized for use in widgets (i.e. we may change the data type to be widget-html rather than general-html)
The toStringAux can definitley need some work if you want to output pretty HTML but in principle you only need this file which as you can see has no dependencies to doc-gen itself.
The file is quite small, you could probably just copy it into another project. I am not sure it is worth maintaining a single dsl-library for different use cases
I think we've added quite a few new features to the doc-gen4 version after it was forked from the widget code, so you probably want to copy the doc-gen4 version.
As a nice exercise before bedtime I wanted to try to use this JSX code. But it doesn't support boolean attributed or the <!DOCTYPE html> tag. So I decided it would make a nice exercise. And of course I failed. I'm trying to edit https://github.com/leanprover/doc-gen4/blob/main/DocGen4/Output/ToHtmlFormat.lean. The dumbest addition I tried was to add
Here is the full thing (depending on nothing outside core Lean):
/-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-/importLean.Data.JsonimportLean.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. -/openLeaninductiveHtmlwhere-- 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)→ArrayHtml→Html|text:String→HtmlderivingRepr,BEq,Inhabited,FromJson,ToJsoninstance:CoeStringHtml:=⟨Html.text⟩namespaceHtmldefattributesToString(attrs:Array(String×String)):String:=attrs.foldl(funacc(k,v)=>acc++" "++k++"=\""++v++"\"")""-- TODO: Termination proofpartialdeftoStringAux:Html→String|elementtagfalseattrs#[texts]=>s!"<{tag}{attributesToString attrs}>{s}</{tag}>\n"|elementtagfalseattrs#[child]=>s!"<{tag}{attributesToString attrs}>\n{child.toStringAux}</{tag}>\n"|elementtagfalseattrschildren=>s!"<{tag}{attributesToString attrs}>\n{children.foldl (· ++ toStringAux ·) ""}</{tag}>\n"|elementtagtrueattrschildren=>s!"<{tag}{attributesToString attrs}>{children.foldl (· ++ toStringAux ·) ""}</{tag}>"|texts=>sdeftoString(html:Html):String:=html.toStringAux.trimRightinstance:ToStringHtml:=⟨toString⟩partialdeftextLength:Html→Nat|texts=>s.length|element___children=>letlengths:=children.maptextLengthlengths.foldlNat.add0defescapePairs:Array(String×String):=#[("&","&"),("<","<"),(">",">"),("\"",""")]defescape(s:String):String:=escapePairs.foldl(funacc(o,r)=>acc.replaceor)sendHtmlnamespaceJsxopenParserPrettyPrinterdeclare_syntax_catjsxElementdeclare_syntax_catjsxChild-- JSXTextCharacter : SourceCharacter but not one of {, <, > or }defjsxText:Parser:=withAntiquot(mkAntiquot"jsxText"`jsxText){fn:=funcs=>letstartPos:=s.poslets:=takeWhile1Fn(not∘"[{<>}]$".contains)"expected JSX text"csmkNodeToken`jsxTextstartPoscs}@[combinator_formatter Jsx.jsxText]defjsxText.formatter:Formatter:=pure()@[combinator_parenthesizer Jsx.jsxText]defjsxText.parenthesizer:Parenthesizer:=pure()syntaxjsxAttrName:=rawIdent<|>strsyntaxjsxAttrVal:=str<|>group("{"term"}")syntaxjsxSimpleAttr:=jsxAttrName"="jsxAttrValsyntaxjsxBoolAttr:=strsyntaxjsxAttrSpread:="["term"]"syntaxjsxAttr:=jsxSimpleAttr<|>jsxAttrSpread<|>jsxBoolAttrsyntax"<!DOCTYPE html>":jsxElementsyntax"<"rawIdentjsxAttr*"/>":jsxElementsyntax"<"rawIdentjsxAttr*">"jsxChild*"</"rawIdent">":jsxElementsyntaxjsxText:jsxChildsyntax"{"term"}":jsxChildsyntax"["term"]":jsxChildsyntaxjsxElement:jsxChildscopedsyntax:maxjsxElement:termdeftranslateAttrs(attrs:Array(TSyntax`Jsx.jsxAttr)):MacroM(TSyntax`term):=doletmutas←`(#[])forattrinattrs.mapTSyntax.rawdoas←matchattrwith|`(jsxAttr|$n:jsxAttrName=$v:jsxAttrVal)=>letn←matchnwith|`(jsxAttrName|$n:str)=>puren|`(jsxAttrName|$n:ident)=>pure<|quote(toStringn.getId)|_=>Macro.throwUnsupportedletv←matchvwith|`(jsxAttrVal|{$v})=>purev|`(jsxAttrVal|$v:str)=>purev|_=>Macro.throwUnsupported`(($as).push($n,($v:String)))|`(jsxAttr|[$t])=>`($as++($t:Array(String×String)))|`(jsxBoolAttr|$n:str)=>puren|_=>Macro.throwUnsupportedreturnasprivatedefhtmlHelper(n:Syntax)(children:ArraySyntax)(m:Syntax):MacroM(String×(TSyntax`term)):=dounlessn.getId==m.getIddowithRefm<|Macro.throwErrors!"Leading and trailing part of tags don't match: '{n}', '{m}'"letmutcs←`(#[])forchildinchildrendocs←matchchildwith|`(jsxChild|$t:jsxText)=>`(($cs).push(Html.text$(quotet.raw[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:ArrayHtml))|`(jsxChild|$e:jsxElement)=>`(($cs).push($e:jsxElement:Html))|_=>Macro.throwUnsupportedlettag:=toStringn.getIdpure<|(tag,cs)macro_rules|`("<!DOCTYPE html>")=>`(Html.element"!DOCTYPE"true#[("html","")]#[])|`(<$n$attrs*/>)=>doletkind:=quote(toStringn.getId)letattrs←translateAttrsattrs`(Html.element$kindtrue$attrs#[])|`(<$n$attrs*>$children*</$m>)=>dolet(tag,children)←htmlHelpernchildrenm`(Html.element$(quotetag)true$(←translateAttrsattrs)$children)endJsx/-- A type which implements `ToHtmlFormat` will be visualizedas the resulting HTML in editors which support it. -/classToHtmlFormat(α:Typeu)whereformatHtml:α→HtmlopenJsxinexample:Html:=<!DOCTYPEhtml>
Based on https://github.com/facebook/react/issues/1035 it seems that <!doctype html> is not supported by JSX either. Another reasonable design would be a HtmlDocument type that just injects that string as a prefix when written out to a file
I give up boolean arguments for now. My best effort is:
/-
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. -/
open Lean
inductive HtmlAttribute where
| keyVal : String → String → HtmlAttribute
| bool : String → HtmlAttribute
deriving Repr, BEq, Inhabited, FromJson, ToJson
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) (boolAttrs) (children : Array Html)
| element : String → Bool → Array HtmlAttribute → Array Html → Html
| text : String → Html
deriving Repr, BEq, Inhabited, FromJson, ToJson
instance : Coe String Html :=
⟨Html.text⟩
namespace Html
def attributesToString (attrs : Array HtmlAttribute) :String :=
attrs.foldl (fun acc attr => match attr with | .keyVal k v => s!"{acc} {k}=\"{v}\"" | .bool a => s!"{acc} {a}") ""
-- 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) :=
#[
("&", "&"),
("<", "<"),
(">", ">"),
("\"", """)
]
def escape (s : String) : String :=
escapePairs.foldl (fun 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 }
@[combinator_formatter Jsx.jsxText] def jsxText.formatter : Formatter := pure ()
@[combinator_parenthesizer Jsx.jsxText] def jsxText.parenthesizer : Parenthesizer := pure ()
syntax jsxAttrName := rawIdent <|> str
syntax jsxAttrVal := str <|> group("{" term "}")
syntax jsxSimpleAttr := jsxAttrName ("=" jsxAttrVal)?
syntax jsxAttrSpread := "[" term "]"
syntax jsxAttr := jsxSimpleAttr <|> jsxAttrSpread
syntax "<!DOCTYPE html>" : jsxElement
syntax "<" rawIdent jsxAttr* "/>" : jsxElement
syntax "<" rawIdent jsxAttr* ">" jsxChild* "</" rawIdent ">" : jsxElement
syntax jsxText : jsxChild
syntax "{" term "}" : jsxChild
syntax "[" term "]" : jsxChild
syntax jsxElement : jsxChild
scoped syntax:max jsxElement : term
def translateAttrs (attrs : Array (TSyntax `Jsx.jsxAttr)) : MacroM (TSyntax `term) := do
let mut as ← `(#[])
for attr in attrs.map TSyntax.raw do
as ← match attr with
| `(jsxAttrName| $n:jsxAttrName) =>
let n ← match n with
| `(jsxAttrName| $n:str) => pure n
| `(jsxAttrName| $n:ident) => pure <| quote (toString n.getId)
| _ => Macro.throwUnsupported
`(HtmlAttribute.bool $n)
| `(jsxAttr| $n:jsxAttrName=$v:jsxAttrVal) =>
let n ← match n with
| `(jsxAttrName| $n:str) => pure n
| `(jsxAttrName| $n:ident) => pure <| quote (toString n.getId)
| _ => Macro.throwUnsupported
let v ← match v with
| `(jsxAttrVal| {$v}) => pure v
| `(jsxAttrVal| $v:str) => pure v
| _ => Macro.throwUnsupported
`(($as).push <| HtmlAttribute.keyVal $n ($v : String))
| `(jsxAttr| [$t]) => `($as ++ ($t : Array (String × String)))
| _ => Macro.throwUnsupported
return as
private def htmlHelper (n : Syntax) (children : Array Syntax) (m : Syntax) : MacroM (String × (TSyntax `term)):= 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.raw[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
| `(<!DOCTYPE html>) => `(Html.element "!DOCTYPE" true #[.bool "html"] #[])
| `(<$n $attrs* />) => do
let kind := quote (toString n.getId)
let attrs ← translateAttrs attrs
`(Html.element $kind true $attrs #[])
| `(<$n $attrs* >$children*</$m>) => do
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
open Jsx
#eval <!DOCTYPE html>
#eval <script src="foo"/>
#eval <script src="bar" async/>