Open bkiefer opened 5 years ago
First and foremost: all fonts should be configurable, in a way that allows "relative" specifications, e.g., "2pt bigger than font for x, and bold" Maybe also colours.
Maybe we should have sth in the EditorConfig like getFontForElement(ELEMENT_ID), and ELEMENT_ID be sth like LOWER_CODE_AREA
getFontForElement(ELEMENT_ID)
ELEMENT_ID
LOWER_CODE_AREA
First and foremost: all fonts should be configurable, in a way that allows "relative" specifications, e.g., "2pt bigger than font for x, and bold" Maybe also colours.