# 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))))