agda-mode
agda-mode copied to clipboard
use user editor font information
I’m one of those crazy weirdos who happen to prefer to write programs in a proportional typeface. It would be really cool if the package could respect the font I chose for my editor.
I was able to do this myself by having the following in my styles.less
file, but I feel like it would be preferable if this was done by the package itself.
.agda-body-container
{
font-family: var(--editor-font-family) !important;
font-size: var(--editor-font-size) !important;
line-height: var(--editor-line-height) !important;
}
Wow I don't know we can do this!
@Zambonifofex I'm rewriting the stylesheet and basing the constants on these variables. But as for --editor-line-height
I can't find any way to change and test it. Do you know how to change them?
It’s in the editor configurations. The setting is called “line height”. (Very offputtingly, settings in Atom are ordered alphabetically, so related settings are not grouped together.)
Ahh, I see! Thanks for the prompt reply 😊