src/Tools/jEdit/src/html_panel.scala
changeset 45099 67740480cf39
parent 43669 9d34288e9351
child 45666 d83797ef0d2d
     1.1 --- a/src/Tools/jEdit/src/html_panel.scala	Tue Sep 27 21:39:55 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/html_panel.scala	Tue Sep 27 22:14:15 2011 +0200
     1.3 @@ -113,7 +113,7 @@
     1.4    /* internal messages */
     1.5  
     1.6    private case class Resize(font_family: String, font_size: Int)
     1.7 -  private case class Render_Document(text: String)
     1.8 +  private case class Render_Document(url: String, text: String)
     1.9    private case class Render(body: XML.Body)
    1.10    private case class Render_Sync(body: XML.Body)
    1.11    private case object Refresh
    1.12 @@ -151,9 +151,9 @@
    1.13  
    1.14      def refresh() { render(current_body) }
    1.15  
    1.16 -    def render_document(text: String)
    1.17 +    def render_document(url: String, text: String)
    1.18      {
    1.19 -      val doc = builder.parse(new InputSourceImpl(new StringReader(text), "http://localhost"))
    1.20 +      val doc = builder.parse(new InputSourceImpl(new StringReader(text), url))
    1.21        Swing_Thread.later { setDocument(doc, rcontext) }
    1.22      }
    1.23  
    1.24 @@ -183,7 +183,7 @@
    1.25        react {
    1.26          case Resize(font_family, font_size) => resize(font_family, font_size)
    1.27          case Refresh => refresh()
    1.28 -        case Render_Document(text) => render_document(text)
    1.29 +        case Render_Document(url, text) => render_document(url, text)
    1.30          case Render(body) => render(body)
    1.31          case Render_Sync(body) => render(body); reply(())
    1.32          case bad => System.err.println("main_actor: ignoring bad message " + bad)
    1.33 @@ -196,7 +196,7 @@
    1.34  
    1.35    def resize(font_family: String, font_size: Int) { main_actor ! Resize(font_family, font_size) }
    1.36    def refresh() { main_actor ! Refresh }
    1.37 -  def render_document(text: String) { main_actor ! Render_Document(text) }
    1.38 +  def render_document(url: String, text: String) { main_actor ! Render_Document(url, text) }
    1.39    def render(body: XML.Body) { main_actor ! Render(body) }
    1.40    def render_sync(body: XML.Body) { main_actor !? Render_Sync(body) }
    1.41  }