chore: use upstream HTML type - #974
Conversation
|
|
||
| {docstring Html.visitM} | ||
|
|
||
| {docstring Html.format} |
There was a problem hiding this comment.
This function has actually been deleted, since nothing in Verso uses it. Let me know if you'd rather keep it.
There was a problem hiding this comment.
That's fine. It used to be used in tests to get more readable output IIRC, but we can get rid of it. It wasn't correct WRT whitespace-sensitive tags anyway.
|
Given that lots of external codebases use this library, I think we should endeavor to provide deprecated aliases for all the names that point at the Lean versions, to make adaptation less painful. |
| If the HTML is not a single tag, no changes are made. | ||
| -/ | ||
| public def Html.setAttribute (attr : String) (value : String) (html : Html) : Html := | ||
| public def setAttribute (attr : String) (value : String) (html : Html) : Html := |
There was a problem hiding this comment.
This is also used downstream, so a deprecated alias in the old namespace would be nice.
|
|
||
| public section | ||
| /-- The default `DOCTYPE` for HTML5. -/ | ||
| public abbrev doctype := "<!DOCTYPE html>" |
There was a problem hiding this comment.
Does this really belong in Lean.Html?
|
|
||
| end Lean.Html | ||
|
|
||
| /-! ## JSX-like syntax -/ |
There was a problem hiding this comment.
Historically, this was at least as inspired by Handlebars and Django templates :-)
2 participants
This PR switches Verso to use the upcoming core Lean HTML type rather than defining one.
JSX-like syntax and utilites are not changed here.