use user editor font information

[ghost]

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;
}

[banacorn]

Wow I don't know we can do this!

[banacorn]

@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?

[ghost]

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.)

[banacorn]

Ahh, I see! Thanks for the prompt reply 😊