# HG changeset patch
# User wenzelm
# Date 1396871712 -7200
# Node ID f0592485b7fbb60d5042097151b7133cbeb5b618
# Parent  34480050397423e7d58c1dd0548f62012e8cd04b
support for URL as file name, similar to treatment in jEdit.java;

diff -r 344800503974 -r f0592485b7fb src/Pure/PIDE/protocol.scala
--- 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,
diff -r 344800503974 -r f0592485b7fb src/Pure/System/isabelle_system.scala
--- 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 */