# HG changeset patch
# User wenzelm
# Date 1353594147 -3600
# Node ID 2585c81d840af42ff4ea9e15d43752013717d575
# Parent  24d47733975f683c0946fdfa74752d6d8433e91c
take component width as indication if it is already visible/layed-out, to avoid multiple formatting with minimal margin;

diff -r 24d47733975f -r 2585c81d840a src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Thu Nov 22 14:53:02 2012 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Thu Nov 22 15:22:27 2012 +0100
@@ -72,38 +72,40 @@
   {
     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
+      val font_metrics = getPainter.getFontMetrics(font)
+      val margin = (getWidth / (font_metrics.charWidth(Pretty.spc) max 1) - 2) max 20
 
-    val base_snapshot = current_base_snapshot
-    val formatted_body = Pretty.formatted(current_body, margin, Pretty.font_metric(font_metrics))
+      val base_snapshot = current_base_snapshot
+      val formatted_body = Pretty.formatted(current_body, margin, Pretty.font_metric(font_metrics))
 
-    future_rendering.map(_.cancel(true))
-    future_rendering = Some(default_thread_pool.submit(() =>
-      {
-        val (text, rendering) = Pretty_Text_Area.text_rendering(base_snapshot, formatted_body)
-        Simple_Thread.interrupted_exception()
+      future_rendering.map(_.cancel(true))
+      future_rendering = Some(default_thread_pool.submit(() =>
+        {
+          val (text, rendering) = Pretty_Text_Area.text_rendering(base_snapshot, formatted_body)
+          Simple_Thread.interrupted_exception()
 
-        Swing_Thread.later {
-          current_rendering = rendering
+          Swing_Thread.later {
+            current_rendering = rendering
 
-          try {
-            getBuffer.beginCompoundEdit
-            getBuffer.setReadOnly(false)
-            setText(text)
-            setCaretPosition(0)
-            getBuffer.setReadOnly(true)
+            try {
+              getBuffer.beginCompoundEdit
+              getBuffer.setReadOnly(false)
+              setText(text)
+              setCaretPosition(0)
+              getBuffer.setReadOnly(true)
+            }
+            finally {
+              getBuffer.endCompoundEdit
+            }
           }
-          finally {
-            getBuffer.endCompoundEdit
-          }
-        }
-      }))
+        }))
+    }
   }
 
   def resize(font_family: String, font_size: Int)