always refresh font metrics, to help window size calculation (amending 2585c81d840a);

--- a/src/Tools/jEdit/src/pretty_text_area.scala	Thu Nov 22 16:55:53 2012 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Thu Nov 22 17:01:20 2012 +0100
@@ -72,12 +72,12 @@
   {
     Swing_Thread.require()
 
+    val font = new Font(current_font_family, Font.PLAIN, current_font_size)
+    getPainter.setFont(font)
+    getPainter.setAntiAlias(new AntiAlias(jEdit.getProperty("view.antiAlias")))
+    getPainter.setStyles(SyntaxUtilities.loadStyles(current_font_family, current_font_size))
+
     if (getWidth > 0) {
-      val font = new Font(current_font_family, Font.PLAIN, current_font_size)
-      getPainter.setFont(font)
-      getPainter.setAntiAlias(new AntiAlias(jEdit.getProperty("view.antiAlias")))
-      getPainter.setStyles(SyntaxUtilities.loadStyles(current_font_family, current_font_size))
-
       val font_metrics = getPainter.getFontMetrics(font)
       val margin = (getWidth / (font_metrics.charWidth(Pretty.spc) max 1) - 2) max 20