support for URL as file name, similar to treatment in jEdit.java;
authorwenzelm
Mon Apr 07 13:55:12 2014 +0200 (2014-04-07)
changeset 56449f0592485b7fb
parent 56448 344800503974
child 56450 16d4213d4cbc
support for URL as file name, similar to treatment in jEdit.java;
src/Pure/PIDE/protocol.scala
src/Pure/System/isabelle_system.scala
     1.1 --- a/src/Pure/PIDE/protocol.scala	Mon Apr 07 13:11:31 2014 +0200
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Mon Apr 07 13:55:12 2014 +0200
     1.3 @@ -353,7 +353,7 @@
     1.4          variant(List(
     1.5            { case Exn.Res((a, b)) =>
     1.6                (Nil, triple(string, string, option(string))(
     1.7 -                (a.node, Isabelle_System.posix_path(a.node), b.map(p => p._1.toString)))) },
     1.8 +                (a.node, Isabelle_System.posix_path_url(a.node), b.map(p => p._1.toString)))) },
     1.9            { case Exn.Exn(e) => (Nil, string(Exn.message(e))) }))
    1.10        YXML.string_of_body(list(encode_blob)(command.blobs))
    1.11      }
    1.12 @@ -384,7 +384,7 @@
    1.13          variant(List(
    1.14            { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
    1.15            { case Document.Node.Deps(header) =>
    1.16 -              val master_dir = Isabelle_System.posix_path(name.master_dir)
    1.17 +              val master_dir = Isabelle_System.posix_path_url(name.master_dir)
    1.18                val imports = header.imports.map(_.node)
    1.19                val keywords = header.keywords.map({ case (a, b, _) => (a, b) })
    1.20                (Nil,
     2.1 --- a/src/Pure/System/isabelle_system.scala	Mon Apr 07 13:11:31 2014 +0200
     2.2 +++ b/src/Pure/System/isabelle_system.scala	Mon Apr 07 13:55:12 2014 +0200
     2.3 @@ -12,6 +12,7 @@
     2.4  import java.io.{File => JFile, BufferedReader, InputStreamReader,
     2.5    BufferedWriter, OutputStreamWriter}
     2.6  import java.nio.file.Files
     2.7 +import java.net.{URL, URLDecoder, MalformedURLException}
     2.8  
     2.9  import scala.util.matching.Regex
    2.10  
    2.11 @@ -190,6 +191,15 @@
    2.12  
    2.13    def posix_path(file: JFile): String = posix_path(file.getPath)
    2.14  
    2.15 +  def posix_path_url(name: String): String =
    2.16 +    try {
    2.17 +      val url = new URL(name)
    2.18 +      if (url.getProtocol == "file")
    2.19 +        posix_path(URLDecoder.decode(url.getPath, UTF8.charset_name))
    2.20 +      else name
    2.21 +    }
    2.22 +    catch { case _: MalformedURLException => posix_path(name) }
    2.23 +
    2.24  
    2.25    /* misc path specifications */
    2.26