I wanted semantic markup. HTML is just a bad source format. It should be the target of a rendering step.
If one really needs to copy the brackets, you can use the print preview of the browser and copy from there. But I am also fine if someone sends Arthur a patch adding all these brackets by hand.
On Wed, Dec 13, 2023 at 4:34 PM Marc Nieper-Wißkirchen <
xxxxxx@gmail.com> wrote:
This is a shortcoming of HTML. I had to use CSS to define some kind of "token" macro. If I could decide, we would be writing SRFIs in SrFiTeX. :)
What's wrong with including #x27E8 and #x2739 characters in the content. either directly as Unicode or as HTML character references (prefixed by ampersands)?