Review handling of proportional and monospace fonts

[aadcg]

Closes #3307.
Closes #3314.
Closes #3315.

[jmercouris]

I didn't make this change because it changed A LOT of the UI, including the describe interface. I'll look at it closely.

[jmercouris]

I tested this, and interestingly enough, now noto sans was being set in the status buffer. I have no idea why this is. This is for sure not the solution!

[aadcg]

Is there a font (technically it couldn't be called a single font) that delivers both proportional and monospaced versions?

[aadcg]

I tested this, and interestingly enough, now noto sans was being set in the status buffer. I have no idea why this is. This is for sure not the solution!

I have an idea why (didn't check). We sometimes place style elements outside head (which is a bad practice).

[jmercouris]

Is there a font (technically it couldn't be called a single font) that delivers both proportional and monospaced versions?

I do believe that there exists a monospaced version of public sans.

[jmercouris]

On second search I've been unable to find a reference to monospace version of Public Sans.

[jmercouris]

Is there a font (technically it couldn't be called a single font) that delivers both proportional and monospaced versions?

Yes there is. However, I haven't really liked how they look. I have found that Bitstream Vera Sans works really well with Public Sans. I'll submit a pull request.

[aadcg]

(@aadcg) I have an idea why (didn't check). We sometimes place style elements outside head (which is a bad practice).

This suggestion of mine is completely unrelated.

I tested this, and interestingly enough, now noto sans was being set in the status buffer. I have no idea why this is. This is for sure not the solution!

Actually, this is not related to this PR or the reported issue. Public Sans wasn't set for the status buffer from the moment when it was first developed.

[aadcg]

I've refactored this PR, and I still think it's superior to #3313. The addition of Public Sans brought a distinctive proportional font for our interfaces. The issue we're trying to solve is that our interfaces can't prevent the renderer from using monospaced fonts for elements that use those by default (such as code or pre). I don't see the need to ship a monospaced font, as #3313 does. I believe it brings added complexity for little gain.

Commit e399b7f is justified by the fact that we currently don't make use of font-weight other than 400 or 700 (regular and bold, respectively) and are unlikely to do so in the future.

[aadcg]

@jmercouris should be ready to be merged.

[aadcg]

I'll merge this on Monday morning the latest to make sure that it lands on the next release.

[jmercouris]

I've added a commit that addresses the size of the prompt buffer fonts. I didn't want to force push on you, so feel free to include it however you like in the commit history. This is important for making things look reasonably sized.

[aadcg]

I've added a commit that addresses the size of the prompt buffer fonts.

I've set the value of 14px for monospace and proportional fonts in a more succinct way for the prompt buffer. You've missed another instance of suggestion/mark count that should use monospaced fonts and I've fixed it.

Note that the reason why I have set initially 16px/14px for proportional/monospace in the prompt buffer is because that's what you did for all other buffer UIs (in #3313).