Conal-Tuohy / jEdit-TEIPlugin

A plugin for the jEdit editor to help support text encoding
6 stars 0 forks source link

More padding around element / attribute names in dropdown boxes. #22

Open jamescummings opened 4 years ago

jamescummings commented 4 years ago

Currently when you add an element or attribute the dropdown menu box seems to have no padding around the element/attribute names (left and right) and is sized to the longest element or attribute name. It would look nicer, I think, and be clearer if there was 3-4px either side of these names. (Or maybe 'one space' if layout isn't done in such a css way.)