If I wanted to have lines of different heights what would be the safest, most consistent approach? It says in the manual that vertical padding is not possible while styling. Is there anything else I could use?
line-height or just
font-size should work.
If I wanted to have vertical spacing between different types of lines that had been decorated with css classes is there a strategy I should try?
Actually, where does it say you can’t add vertical padding?
I noticed the scrolling became jumpy if I added asymmetrical padding to a line.
I can see how you could interpret that sentence that way, but it is just trying to explain how to add document-wide padding. I’ve rephrased it a bit.
I’m not noticing jumpy scrolling in this setup.
Thanks for the help. I had added some sub-optimal css to a gutter and that seems to have been the issue.
When I add asymmetrical padding to code mirror with line wrapping the cursor jumps over certain lines if I arrow up or down.
Thanks for the example. This patch should help with that.