src/Pure/General/file.scala

--- a/src/Pure/General/file.scala	Tue Jan 03 23:21:09 2017 +0100
+++ b/src/Pure/General/file.scala	Wed Jan 04 12:03:45 2017 +0100
@@ -13,7 +13,7 @@
 import java.nio.file.{StandardOpenOption, StandardCopyOption, Path => JPath,
   Files, SimpleFileVisitor, FileVisitResult}
 import java.nio.file.attribute.BasicFileAttributes
-import java.net.{URL, URLDecoder, MalformedURLException}
+import java.net.{URL, MalformedURLException}
 import java.util.zip.{GZIPInputStream, GZIPOutputStream}
 import java.util.regex.Pattern
 
@@ -33,7 +33,7 @@
     if (Platform.is_windows) {
       val Platform_Root = new Regex("(?i)" +
         Pattern.quote(Isabelle_System.cygwin_root()) + """(?:\\+|\z)(.*)""")
-      val Drive = new Regex("""\\?([a-zA-Z]):\\*(.*)""")
+      val Drive = new Regex("""([a-zA-Z]):\\*(.*)""")
 
       platform_path.replace('/', '\\') match {
         case Platform_Root(rest) => "/" + rest.replace('\\', '/')
@@ -53,8 +53,8 @@
   def standard_url(name: String): String =
     try {
       val url = new URL(name)
-      if (url.getProtocol == "file")
-        standard_path(URLDecoder.decode(url.getPath, UTF8.charset_name))
+      if (url.getProtocol == "file" && Url.is_wellformed_file(name))
+        standard_path(Url.parse_file(name))
       else name
     }
     catch { case _: MalformedURLException => standard_path(name) }