src/Tools/jEdit/src/jedit/html_panel.scala

   /** main actor **/
 
   /* internal messages */
 
   private case class Resize(font_family: String, font_size: Int)
-  private case class Render(body: List[XML.Tree])
+  private case class Render(body: XML.Body)
   private case object Refresh
 
   private val main_actor = actor {
 
     /* internal state */
 
     var current_font_metrics: FontMetrics = null
     var current_font_family = ""
     var current_font_size: Int = 0
     var current_margin: Int = 0
-    var current_body: List[XML.Tree] = Nil
+    var current_body: XML.Body = Nil
 
     def resize(font_family: String, font_size: Int)
     {
       val font = new Font(font_family, Font.PLAIN, lobo_px(raw_px(font_size)))
       val (font_metrics, margin) =

       }
     }
 
     def refresh() { render(current_body) }
 
-    def render(body: List[XML.Tree])
+    def render(body: XML.Body)
     {
       current_body = body
       val html_body =
         current_body.flatMap(div =>
           Pretty.formatted(List(div), current_margin, Pretty.font_metric(current_font_metrics))

 
   /* external methods */
 
   def resize(font_family: String, font_size: Int) { main_actor ! Resize(font_family, font_size) }
   def refresh() { main_actor ! Refresh }
-  def render(body: List[XML.Tree]) { main_actor ! Render(body) }
+  def render(body: XML.Body) { main_actor ! Render(body) }
 }