Henrik Böving
|
0efbcd1f60
|
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.
|
2021-12-25 14:04:35 +01:00 |
|
Henrik Böving
|
03ec9c2e1d
|
chore: Cleanup the JSX parser a bit
|
2021-12-17 15:59:33 +01:00 |
|
Henrik Böving
|
0719fd6e30
|
feat: Allow Array Html as child of an HTMl node
|
2021-12-12 13:38:31 +01:00 |
|
Henrik Böving
|
413a24da56
|
feat: improve HTML to String a bit
|
2021-12-12 13:38:31 +01:00 |
|
Henrik Böving
|
e9a9e17439
|
feat: Basic Html to String converter
It works okay-ish for basic HTML which should be good enough for now
|
2021-12-12 13:38:31 +01:00 |
|
Henrik Böving
|
11de4f7f55
|
chore: Import ToHtmlFormat https://github.com/leanprover/lean4/pull/723
Added some slight modifications so it is inside the DocGen4 instead of
the Lean4.Widget namespace.
|
2021-12-12 13:38:31 +01:00 |