# HG changeset patch
# User wenzelm
# Date 1317155757 -7200
# Node ID 0971c3ee3cdf3646cddcae63bd6a74b334b7f22a
# Parent  67740480cf3985c41168bfb86bedca16681ac3f3
proper platform_file_url;

diff -r 67740480cf39 -r 0971c3ee3cdf src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Tue Sep 27 22:14:15 2011 +0200
+++ b/src/Pure/System/isabelle_system.scala	Tue Sep 27 22:35:57 2011 +0200
@@ -110,6 +110,16 @@
   def platform_path(path: Path): String = standard_system.jvm_path(standard_path(path))
   def platform_file(path: Path): File = new File(platform_path(path))
 
+  def platform_file_url(raw_path: Path): String =
+  {
+    val path = raw_path.expand
+    require(path.is_absolute)
+    val s =
+      if (Platform.is_windows) "/" + platform_path(path).replace('\\', '/')
+      else platform_path(path)
+    "file://" + s.replaceAll(" ", "%20")
+  }
+
   def posix_path(jvm_path: String): String = standard_system.posix_path(jvm_path)
 
 
diff -r 67740480cf39 -r 0971c3ee3cdf src/Tools/jEdit/src/session_dockable.scala
--- a/src/Tools/jEdit/src/session_dockable.scala	Tue Sep 27 22:14:15 2011 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala	Tue Sep 27 22:35:57 2011 +0200
@@ -28,8 +28,9 @@
 
   private val readme = new HTML_Panel("SansSerif", 14)
   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)))
+  readme.render_document(
+    Isabelle_System.platform_file_url(readme_path),
+    Isabelle_System.try_read(List(readme_path)))
 
   val status = new ListView(Nil: List[Document.Node.Name]) {
     listenTo(mouse.clicks)