# HG changeset patch
# User wenzelm
# Date 1353600080 -3600
# Node ID 4a575ef464664e0b63d2e111845cbf32cfb93da9
# Parent  4f2b5b2a9ad58360efc1a195dfb5500b9eda8942
always refresh font metrics, to help window size calculation (amending 2585c81d840a);

diff -r 4f2b5b2a9ad5 -r 4a575ef46466 src/Tools/jEdit/src/pretty_text_area.scala
--- 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