1.1 --- a/src/Tools/jEdit/src/jedit/html_panel.scala	Thu May 20 15:51:28 2010 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit/html_panel.scala	Thu May 20 16:22:50 2010 +0200
     1.3 @@ -105,7 +105,6 @@
     1.4    {
     1.5      var current_font_size: Int = 0
     1.6      var current_font_metrics: FontMetrics = null
     1.7 -    var current_margin: Int = 0
     1.8      var current_body: List[XML.Tree] = Nil
     1.9      var current_DOM: org.w3c.dom.Document = null
    1.10  
    1.11 @@ -116,8 +115,6 @@
    1.12            current_font_size = font_size
    1.13            current_font_metrics =
    1.14              getFontMetrics(system.get_font(lobo_px(raw_px(font_size))))
    1.15 -          current_margin =
    1.16 -            (getWidth() / (current_font_metrics.charWidth(Symbol.spc) max 1) - 4) max 20
    1.17          }
    1.18          current_DOM =
    1.19            builder.parse(
    1.20 @@ -129,9 +126,10 @@
    1.21      def render(body: List[XML.Tree])
    1.22      {
    1.23        current_body = body
    1.24 +      val margin = (getWidth() / (current_font_metrics.charWidth(Symbol.spc) max 1) - 4) max 20
    1.25        val html_body =
    1.26          current_body.flatMap(div =>
    1.27 -          Pretty.formatted(List(div), current_margin,
    1.28 +          Pretty.formatted(List(div), margin,
    1.29                Pretty.font_metric(current_font_metrics))
    1.30              .map(t => XML.elem(HTML.PRE, HTML.spans(t))))
    1.31