- PIDE is an emerging framework for sophisticated Prover IDEs, + PIDE is a novel framework for sophisticated Prover IDEs, based on Isabelle/Scala technology that is integrated with Isabelle. It is build around a concept of asynchronous document processing, which is supported diff -r 37c89c5cc601 -r 67740480cf39 src/Tools/jEdit/src/html_panel.scala --- a/src/Tools/jEdit/src/html_panel.scala Tue Sep 27 21:39:55 2011 +0200 +++ b/src/Tools/jEdit/src/html_panel.scala Tue Sep 27 22:14:15 2011 +0200 @@ -113,7 +113,7 @@ /* internal messages */ private case class Resize(font_family: String, font_size: Int) - private case class Render_Document(text: String) + private case class Render_Document(url: String, text: String) private case class Render(body: XML.Body) private case class Render_Sync(body: XML.Body) private case object Refresh @@ -151,9 +151,9 @@ def refresh() { render(current_body) } - def render_document(text: String) + def render_document(url: String, text: String) { - val doc = builder.parse(new InputSourceImpl(new StringReader(text), "http://localhost")) + val doc = builder.parse(new InputSourceImpl(new StringReader(text), url)) Swing_Thread.later { setDocument(doc, rcontext) } } @@ -183,7 +183,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_Document(url, text) => render_document(url, text) case Render(body) => render(body) case Render_Sync(body) => render(body); reply(()) case bad => System.err.println("main_actor: ignoring bad message " + bad) @@ -196,7 +196,7 @@ 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_document(url: String, text: String) { main_actor ! Render_Document(url, text) } def render(body: XML.Body) { main_actor ! Render(body) } def render_sync(body: XML.Body) { main_actor !? Render_Sync(body) } } diff -r 37c89c5cc601 -r 67740480cf39 src/Tools/jEdit/src/session_dockable.scala --- a/src/Tools/jEdit/src/session_dockable.scala Tue Sep 27 21:39:55 2011 +0200 +++ b/src/Tools/jEdit/src/session_dockable.scala Tue Sep 27 22:14:15 2011 +0200 @@ -27,7 +27,9 @@ /* main tabs */ private val readme = new HTML_Panel("SansSerif", 14) - readme.render_document(Isabelle_System.try_read(List(Path.explode("$JEDIT_HOME/README.html")))) + private val readme_path = Path.explode("$JEDIT_HOME/README.html") + private val readme_url = "file://" + readme_path.expand.implode + readme.render_document(readme_url, Isabelle_System.try_read(List(readme_path))) val status = new ListView(Nil: List[Document.Node.Name]) { listenTo(mouse.clicks)