banacorn / agda-mode

agda-mode on Atom
https://atom.io/packages/agda-mode
MIT License
58 stars 14 forks source link

header text overflows incorrectly #86

Open ghost opened 5 years ago

ghost commented 5 years ago

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

banacorn commented 5 years ago

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

ghost commented 5 years ago

Sure.

Header text overflowing incorrectly

banacorn commented 5 years ago

Thanks, I see!