Changing the Java source editor font changes the size of some values in the JMC tables

For example the values in the Mean browser tab in the console.

These are the problems:

• If we want the fonts in JMC to follow the editor font size we should probably adjust all font sizes
• A better idea would probably be have them independent but allow for font size changes using the same keyboard shortcut as for adjusting font sizes in the editor
• All fonts should in any case be adjusted to the same size, not just for one special font
• IIRC there is a problem with the icons in SWT tables, and the row height. Not sure if this is a still an issue, but could be worth bearing in mind.