agda-mode
agda-mode copied to clipboard
header text overflows incorrectly
It seems that if there is not enough space for the header text to fit (e.g. the “All Done” text), it will overflow out of the header, and into clipping the information below (if there is any). This is especially noticeable with large header text (such as “All Goals, Errors”).
I think that either the header should resize to accommodate for the large text, or that the text should fade out to the right (probably using text-overflow: fade
).
It's a little bit hard to picture this, can you please provide us with a screenshot?
Sure.
Thanks, I see!