Inline code should scale with font size

[fredrik-bakke]

This issue is particularly noticeable in the main module headers:

[VojtechStep]

I'll just comment on this for now, if anyone wants to play with this — I unknowingly introduced this in #1154, where I changed the code size from 0.875em to 1.3rem, to fix #1053. The em units are relative to the current element font size, while the rem units are relative to the root element size. This fixed the size difference between Agda code blocks and other code blocks, but as a result all code, inline or not, has the same size.

I don't know if we noticed this before, but the reason why non-Agda code blocks were smaller is because they are in a <code> element nested in a <pre> element, so the scaling down used to be applied twice.

Note that Agda code blocks are just <pre> elements, and inline code blocks are just <code> elements, so we can't very well just remove the rule from one or the other.

[fredrik-bakke]

Are you sure this was introduced in #1154? I thought I had seen this issue before that too, but maybe I'm misremembering.

[VojtechStep]

I'm pretty sure, before that PR the code blocks were relative to the element font size. It's possible that they were still noticeably smaller than the surrounding text in headers, but they were still bigger than normal text.

[VojtechStep]

I know that there were size issues with using the Unicode infinity vs LaTeX infinity, but I think that's because the Unicode one is just small.

[fredrik-bakke]

I'm pretty sure, before that PR the code blocks were relative to the element font size. It's possible that they were still noticeably smaller than the surrounding text in headers, but they were still bigger than normal text.

Right, this might be it.