Plutus book: mapsto

[kwxm]

This is a tiny subset of #1228.

There are a number of places in the book where the mapsto symbol appears. In the source it appears as |->, but in the output it appears as |→, which looks very strange. It turns out that asciidoctor translates certain sequences of characters ("replacements") at an early stage in its processing pipeline, and that one of these sequences is ->, which it turns into the right-arrow character entity, → or → (see https://asciidoctor.org/docs/user-manual/#replacements). So it's managing to deal with part of "|->", but not all of it. What actually appears in the HTML output is |→.

Now HTML5 (but not HTML4) has an entity ↦ or ↦: this appears as ↦ and would be ideal for the job, but unfortunately it doesn't quite work. The basic asciidoctor program handles both ↦ and ↦ perfectly well, producing correct HTML output. However, asciidoctor-pdf can't deal with either of these. If you put ↦ in the source then it produces a pdf with a space where the arrow should be (without complaining). If you use ↦ then you get ERROR: failed to pass formatted text.

I think the problem is just that asciidoctor-pdf just can't handle complicated characters well, and it looks as if this would be something that it would be difficult to fix: see asciidoctor/asciidoctor-pdf#1129 and https://github.com/asciidoctor/asciidoctor-pdf/blob/master/docs/theming-guide.adoc#fonts

Presumably this problem would go away if we solved #1228, and I don't think there's anything we can do to fix it quickly. However it took me a while to work out what was going on, so I thought I'd record it here for posterity. I only looked at the pdf and html output, so I don't know what happens with other formats.

[michaelpj]

I don't have much intention to fix #1228. It would be quite a lot of work, and I don't think we really need much mathematics in the book (TBH, I think we could get rid of of a lot of the stuff that's there at the moment).