agda-mode icon indicating copy to clipboard operation
agda-mode copied to clipboard

header text overflows incorrectly

Open zamfofex opened this issue 5 years ago • 3 comments

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

zamfofex avatar Mar 05 '19 04:03 zamfofex

It's a little bit hard to picture this, can you please provide us with a screenshot?

banacorn avatar Mar 06 '19 06:03 banacorn

Sure.

Header text overflowing incorrectly

zamfofex avatar Mar 06 '19 06:03 zamfofex

Thanks, I see!

banacorn avatar Mar 06 '19 06:03 banacorn