# HG changeset patch
# User wenzelm
# Date 1285164237 -7200
# Node ID 2258769f112f2c235a03cbbadd4e911c63c2355c
# Parent  5b81b8df1ddeb2ebb5f56550e9a2e9811962f438
basic support for full document rendering;

diff -r 5b81b8df1dde -r 2258769f112f src/Tools/jEdit/src/jedit/html_panel.scala
--- a/src/Tools/jEdit/src/jedit/html_panel.scala	Wed Sep 22 15:01:34 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/html_panel.scala	Wed Sep 22 16:03:57 2010 +0200
@@ -116,6 +116,7 @@
   /* internal messages */
 
   private case class Resize(font_family: String, font_size: Int)
+  private case class Render_Document(text: String)
   private case class Render(body: XML.Body)
   private case object Refresh
 
@@ -152,6 +153,12 @@
 
     def refresh() { render(current_body) }
 
+    def render_document(text: String)
+    {
+      val doc = builder.parse(new InputSourceImpl(new StringReader(text), "http://localhost"))
+      Swing_Thread.later { setDocument(doc, rcontext) }
+    }
+
     def render(body: XML.Body)
     {
       current_body = body
@@ -179,6 +186,7 @@
       react {
         case Resize(font_family, font_size) => resize(font_family, font_size)
         case Refresh => refresh()
+        case Render_Document(text) => render_document(text)
         case Render(body) => render(body)
         case bad => System.err.println("main_actor: ignoring bad message " + bad)
       }
@@ -190,5 +198,6 @@
 
   def resize(font_family: String, font_size: Int) { main_actor ! Resize(font_family, font_size) }
   def refresh() { main_actor ! Refresh }
+  def render_document(text: String) { main_actor ! Render_Document(text) }
   def render(body: XML.Body) { main_actor ! Render(body) }
 }