Adjustable font+size (or at least size) for label display

[gwiede]

I find it's often difficult to parse the label / jump-target required in the brief time displayed -- mono fonts tend to be "busy" at edges, so adjacent chars can "merge together" making labels difficult to quickly read.

It would be great if I could adjust the the jump targets / labels to use slightly larger font size, or even a different font entirely from the editor text proper (in order to ease discrimination from that text).