# HG changeset patch
# User wenzelm
# Date 1274365370 -7200
# Node ID 9421452afc29cb99390f11f0d0e5e6d5c2bbf052
# Parent  797af3ebd5f1446e237d20edaf5bb0b1814b2e90
determine margin just before rendering -- proper reformatting when updating;

diff -r 797af3ebd5f1 -r 9421452afc29 src/Tools/jEdit/src/jedit/html_panel.scala
--- a/src/Tools/jEdit/src/jedit/html_panel.scala	Thu May 20 15:51:28 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/html_panel.scala	Thu May 20 16:22:50 2010 +0200
@@ -105,7 +105,6 @@
   {
     var current_font_size: Int = 0
     var current_font_metrics: FontMetrics = null
-    var current_margin: Int = 0
     var current_body: List[XML.Tree] = Nil
     var current_DOM: org.w3c.dom.Document = null
 
@@ -116,8 +115,6 @@
           current_font_size = font_size
           current_font_metrics =
             getFontMetrics(system.get_font(lobo_px(raw_px(font_size))))
-          current_margin =
-            (getWidth() / (current_font_metrics.charWidth(Symbol.spc) max 1) - 4) max 20
         }
         current_DOM =
           builder.parse(
@@ -129,9 +126,10 @@
     def render(body: List[XML.Tree])
     {
       current_body = body
+      val margin = (getWidth() / (current_font_metrics.charWidth(Symbol.spc) max 1) - 4) max 20
       val html_body =
         current_body.flatMap(div =>
-          Pretty.formatted(List(div), current_margin,
+          Pretty.formatted(List(div), margin,
               Pretty.font_metric(current_font_metrics))
             .map(t => XML.elem(HTML.PRE, HTML.spans(t))))