Hmmm, re-thinking it, if the user changes the font size to be able to read it (bigger), or to fit more in (smaller) its reasonable to expect that the margin symbols will expand or contract along with the font size.
But IIUC the problem is that Scintilla modifies the height of symbols automatically as the line height changes, but not the margin width. In fact the margin width constrains the maximum symbol size, resulting in symbols not growing as the font size is increased, and having excess space in the margin when the font size is decreased. As you note, changing a fixed margin width setting as you change font sizes is not very user friendly, but #2140 is better than the original unchangeable width. So the basic idea is sensible, and I see it as an improvement on #2140. So having the width factored by something that depends on the font size is fine. In most cases a fixed fraction is also probably fine, but reading the comments above it appears that the magic number is optimised for our conventional square margin symbols, but if plugins use other symbols with different aspect ratios that could be a reason for making the factor variable. And also some users might just like more space. So there is some purpose for making the factor a setting. Whilst clearly both automatic margin scaling and fixed width cannot be active at once, in theory it would be possible to have both and let the user choose which, but I'm not sure if its worth it, to me the automatic approach is strictly an improvement on a fixed setting, which is of course an improvement on no setting. QED [end thesis] -- You are receiving this because you are subscribed to this thread. Reply to this email directly or view it on GitHub: https://github.com/geany/geany/pull/1738#issuecomment-706117255
