We define a representation of HTML trees together with a JSX-like DSL for writing them.
A HTML tree which may contain widget components.
- element : String → Array (String × Lean.Json) → Array Html → Html
An
element "tag" attrs children
represents<tag {...attrs}>{...children}</tag>
. - text : String → Html
Raw HTML text.
- component : UInt64 → String → LazyEncodable Lean.Json → Array Html → Html
A
component h e props children
represents<Foo {...props}>{...children}</Foo>
, whereFoo : Component Props
is some component such thath = hash Foo.javascript
,e = Foo.«export»
, andprops
will produce a JSON-encoded value of typeProps
.
Instances For
Equations
Instances For
Interpolates an expression into a JSX attribute literal.
Equations
Instances For
Interpolates a collection into a JSX attribute literal.
For HTML tags, this should have type Array (String × Json)
.
For ProofWidgets.Component
s, it can be any structure $t
whatsoever:
it is interpolated into the component's props using { $t with ... }
notation.
Equations
Instances For
Characters not allowed inside JSX plain text.
Equations
Instances For
Equations
Instances For
Equations
Instances For
Interpolates an array of elements into a JSX literal
Equations
Instances For
Interpolates an expression into a JSX literal
Equations
Instances For
Equations
Instances For
First delaborate into our non-term TSyntax
. Note this means we can't call delab
,
so we have to add the term annotations ourselves.
Equations
Instances For
Now wrap our TSyntax _
delaborators into Term
elaborators.