More font sizes

[tod]

Could we allow the user to set an arbitrary font size in the terminal, or at least include larger sizes in the drop down list? I do a lot of text editing in full screen terminal windows on a physically large display. A font size of 36 allows me to keep the display away far from my face while still being able to read the text without glasses. Thanks.

[axeld]

IIRC we restricted the font size for the main fonts since the layout API wasn't used everywhere yet, but there is at least no technical reason to restrict the Terminal.

It would be nice to have some kind of common method to select a font size, though. The current pull down menu approach is a bit restricted, a slider might be too inconvenient in order to set the standard sizes. Maybe have a slider as the last menu item. IIRC John Scipione wanted to work on such a thing for the icon sizes in Tracker -- maybe that work could be reused here.

[Disreali]

Implementing a spinner would be nice. ticket:6834

[jscipione]

I may have made this worse by integrating the font size as a submenu of the font menu. The real solution IMHO is to create a font panel dialog instead of generating the font selecter here. However, since that is a lot of work, perhaps we could just add more font sizes to the list in the interim.

[jscipione]

Fixed in hrev44982 by increasing font size options from 8 to 36. We could go even larger if necessary, there is no good reason to restrict the top font size option other than to keep it in a reasonable range.