# HG changeset patch # User wenzelm # Date 1273656665 -7200 # Node ID fc8a6b5f9b0b64940ef35af60f519cbc4eae5b15 # Parent 599466689412a7f20cd1551ae29f5809d7f48173 format as topmost list of "divs", not just adjacent "spans" -- for proper line breaking; diff -r 599466689412 -r fc8a6b5f9b0b src/Tools/jEdit/src/jedit/html_panel.scala --- a/src/Tools/jEdit/src/jedit/html_panel.scala Wed May 12 11:28:52 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/html_panel.scala Wed May 12 11:31:05 2010 +0200 @@ -119,7 +119,7 @@ private val builder = new DocumentBuilderImpl(ucontext, rcontext) private case class Init(font_size: Int) - private case class Render(body: List[XML.Tree]) + private case class Render(divs: List[XML.Tree]) private val main_actor = actor { // crude double buffering @@ -146,11 +146,12 @@ doc2 = parse() Swing_Thread.now { setDocument(doc1, rcontext) } - case Render(body) => + case Render(divs) => val doc = doc2 val html_body = - Pretty.formatted(body, panel_width(current_font_size), metric) - .map(t => XML.elem(HTML.PRE, HTML.spans(t))) + divs.flatMap(div => + Pretty.formatted(List(div), panel_width(current_font_size), metric) + .map(t => XML.elem(HTML.PRE, HTML.spans(t)))) val node = XML.document_node(doc, XML.elem(HTML.BODY, html_body)) doc.removeChild(doc.getLastChild()) doc.appendChild(node) @@ -167,7 +168,7 @@ /* main method wrappers */ def init(font_size: Int) { main_actor ! Init(font_size) } - def render(body: List[XML.Tree]) { main_actor ! Render(body) } + def render(divs: List[XML.Tree]) { main_actor ! Render(divs) } init(initial_font_size) }