proper platform_file_url;
authorwenzelm
Tue Sep 27 22:35:57 2011 +0200 (2011-09-27)
changeset 451000971c3ee3cdf
parent 45099 67740480cf39
child 45101 6317e969fb30
proper platform_file_url;
src/Pure/System/isabelle_system.scala
src/Tools/jEdit/src/session_dockable.scala
     1.1 --- a/src/Pure/System/isabelle_system.scala	Tue Sep 27 22:14:15 2011 +0200
     1.2 +++ b/src/Pure/System/isabelle_system.scala	Tue Sep 27 22:35:57 2011 +0200
     1.3 @@ -110,6 +110,16 @@
     1.4    def platform_path(path: Path): String = standard_system.jvm_path(standard_path(path))
     1.5    def platform_file(path: Path): File = new File(platform_path(path))
     1.6  
     1.7 +  def platform_file_url(raw_path: Path): String =
     1.8 +  {
     1.9 +    val path = raw_path.expand
    1.10 +    require(path.is_absolute)
    1.11 +    val s =
    1.12 +      if (Platform.is_windows) "/" + platform_path(path).replace('\\', '/')
    1.13 +      else platform_path(path)
    1.14 +    "file://" + s.replaceAll(" ", "%20")
    1.15 +  }
    1.16 +
    1.17    def posix_path(jvm_path: String): String = standard_system.posix_path(jvm_path)
    1.18  
    1.19  
     2.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Tue Sep 27 22:14:15 2011 +0200
     2.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Tue Sep 27 22:35:57 2011 +0200
     2.3 @@ -28,8 +28,9 @@
     2.4  
     2.5    private val readme = new HTML_Panel("SansSerif", 14)
     2.6    private val readme_path = Path.explode("$JEDIT_HOME/README.html")
     2.7 -  private val readme_url = "file://" + readme_path.expand.implode
     2.8 -  readme.render_document(readme_url, Isabelle_System.try_read(List(readme_path)))
     2.9 +  readme.render_document(
    2.10 +    Isabelle_System.platform_file_url(readme_path),
    2.11 +    Isabelle_System.try_read(List(readme_path)))
    2.12  
    2.13    val status = new ListView(Nil: List[Document.Node.Name]) {
    2.14      listenTo(mouse.clicks)