# HG changeset patch
# User wenzelm
# Date 1260302476 -3600
# Node ID 4f9bcd4b5bd1ab12a23909ad9f6df398936f9395
# Parent  63ba7f0931e2e052585986a6ce61fe8cc8eaa282
provide dummy URL;

diff -r 63ba7f0931e2 -r 4f9bcd4b5bd1 src/Tools/jEdit/src/proofdocument/html_panel.scala
--- a/src/Tools/jEdit/src/proofdocument/html_panel.scala	Tue Dec 08 20:14:08 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/html_panel.scala	Tue Dec 08 21:01:16 2009 +0100
@@ -73,7 +73,8 @@
       react {
         case Init(font_size) =>
           val src = template(font_size)
-          def parse() = builder.parse(new InputSourceImpl(new StringReader(src)))
+          def parse() =
+            builder.parse(new InputSourceImpl(new StringReader(src), "http://localhost"))
           doc1 = parse()
           doc2 = parse()
           Swing_Thread.now { setDocument(doc1, rcontext) }