--- a/src/Pure/PIDE/protocol.scala Mon Apr 07 13:11:31 2014 +0200
+++ b/src/Pure/PIDE/protocol.scala Mon Apr 07 13:55:12 2014 +0200
@@ -353,7 +353,7 @@
variant(List(
{ case Exn.Res((a, b)) =>
(Nil, triple(string, string, option(string))(
- (a.node, Isabelle_System.posix_path(a.node), b.map(p => p._1.toString)))) },
+ (a.node, Isabelle_System.posix_path_url(a.node), b.map(p => p._1.toString)))) },
{ case Exn.Exn(e) => (Nil, string(Exn.message(e))) }))
YXML.string_of_body(list(encode_blob)(command.blobs))
}
@@ -384,7 +384,7 @@
variant(List(
{ case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
{ case Document.Node.Deps(header) =>
- val master_dir = Isabelle_System.posix_path(name.master_dir)
+ val master_dir = Isabelle_System.posix_path_url(name.master_dir)
val imports = header.imports.map(_.node)
val keywords = header.keywords.map({ case (a, b, _) => (a, b) })
(Nil,
--- a/src/Pure/System/isabelle_system.scala Mon Apr 07 13:11:31 2014 +0200
+++ b/src/Pure/System/isabelle_system.scala Mon Apr 07 13:55:12 2014 +0200
@@ -12,6 +12,7 @@
import java.io.{File => JFile, BufferedReader, InputStreamReader,
BufferedWriter, OutputStreamWriter}
import java.nio.file.Files
+import java.net.{URL, URLDecoder, MalformedURLException}
import scala.util.matching.Regex
@@ -190,6 +191,15 @@
def posix_path(file: JFile): String = posix_path(file.getPath)
+ def posix_path_url(name: String): String =
+ try {
+ val url = new URL(name)
+ if (url.getProtocol == "file")
+ posix_path(URLDecoder.decode(url.getPath, UTF8.charset_name))
+ else name
+ }
+ catch { case _: MalformedURLException => posix_path(name) }
+
/* misc path specifications */