YOU CAN NOW CHANGE YOUR TERMINAL FONT SIZE (independent of the global font size).  This should be very useful for fonts that show up unusually large or small by default.
app_terminal.py:  Changed TerminalApplication.get_font() from using a single argument of 'font' to using a single argument of 'settings' which must contain a 'font_family' key/value and optionally may contain a 'font_size' key/value.
terminal.js:  Updated GateOne.Terminal.loadFont() to use the new 'settings' format for the 'terminal:get_font' WebSocket action (as noted above).
terminal.js:  Added the ability to change the size of your chosen font via a simple input element in the preferences panel.
terminal.js:  Renamed GateOne.prefs.font (which is only used by the terminal application) to GateOne.prefs.terminalFont.  This makes more sense since you can now control your terminal font size independently of GateOne's global GateOne.prefs.fontSize.
font.css:  Added 'font-size' which uses the 'font_size' variable.
Themes:  Removed the hard-coded font-size property on '.✈terminal pre'.