Binary file src/Tools/jEdit/PIDE.png has changed
--- a/src/Tools/jEdit/README.html Tue Sep 27 21:39:55 2011 +0200
+++ b/src/Tools/jEdit/README.html Tue Sep 27 22:14:15 2011 +0200
@@ -12,10 +12,10 @@
<body>
-<h2>The PIDE framework</h2>
+<center><h2><img alt="PIDE" src="PIDE.png" width="230" align="middle"/></h2></center>
<p>
- <b>PIDE</b> is an emerging framework for sophisticated Prover IDEs,
+ <b>PIDE</b> 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
<em>asynchronous document processing</em>, which is supported
--- 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) }
}
--- 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)
