# HG changeset patch
# User wenzelm
# Date 1483527825 -3600
# Node ID dd3797f1e0d61e44c9c00df1f29865bc8049ba81
# Parent  1ddc262514b8d5d6ccc8438fba175c340feec6bc
clarified file URIs;

diff -r 1ddc262514b8 -r dd3797f1e0d6 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) }
diff -r 1ddc262514b8 -r dd3797f1e0d6 src/Pure/General/url.scala
--- a/src/Pure/General/url.scala	Tue Jan 03 23:21:09 2017 +0100
+++ b/src/Pure/General/url.scala	Wed Jan 04 12:03:45 2017 +0100
@@ -8,6 +8,7 @@
 
 
 import java.io.{File => JFile}
+import java.nio.file.Paths
 import java.net.{URI, URISyntaxException}
 import java.net.{URL, MalformedURLException}
 import java.util.zip.GZIPInputStream
@@ -51,36 +52,15 @@
 
   /* file URIs */
 
-  def file(uri: String): JFile = new JFile(new URI(uri))
+  def print_file(file: JFile): String =
+    file.toPath.toAbsolutePath.toUri.normalize.toString
+
+  def parse_file(uri: String): JFile = Paths.get(new URI(uri)).toFile
 
   def is_wellformed_file(uri: String): Boolean =
-    try { file(uri); true }
+    try { parse_file(uri); true }
     catch { case _: URISyntaxException | _: IllegalArgumentException => false }
 
   def normalize_file(uri: String): String =
-    if (is_wellformed_file(uri)) {
-      val uri1 = new URI(uri).normalize.toASCIIString
-      if (uri1.startsWith("file://")) uri1
-      else {
-        Library.try_unprefix("file:/", uri1) match {
-          case Some(p) => "file:///" + p
-          case None => uri1
-        }
-      }
-    }
-    else uri
-
-  def platform_file(path: Path): String =
-  {
-    val path1 = path.expand
-    require(path1.is_absolute)
-    platform_file(File.platform_path(path1))
-  }
-
-  def platform_file(name: String): String =
-    if (name.startsWith("file://")) name
-    else {
-      val s = name.replaceAll(" ", "%20")
-      "file://" + (if (Platform.is_windows) s.replace('\\', '/') else s)
-    }
+    if (is_wellformed_file(uri)) print_file(parse_file(uri)) else uri
 }
diff -r 1ddc262514b8 -r dd3797f1e0d6 src/Tools/VSCode/src/document_model.scala
--- a/src/Tools/VSCode/src/document_model.scala	Tue Jan 03 23:21:09 2017 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Wed Jan 04 12:03:45 2017 +0100
@@ -45,7 +45,7 @@
 
   /* external file */
 
-  val file: JFile = Url.file(uri).getCanonicalFile
+  val file: JFile = Url.parse_file(uri).getCanonicalFile
 
   def external(b: Boolean): Document_Model = copy(external_file = b)
 
diff -r 1ddc262514b8 -r dd3797f1e0d6 src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Tue Jan 03 23:21:09 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Wed Jan 04 12:03:45 2017 +0100
@@ -79,12 +79,16 @@
   def hyperlink_source_file(source_name: String, line1: Int, range: Symbol.Range)
     : Option[Line.Node_Range] =
   {
-    for (name <- resources.source_file(source_name))
+    for {
+      name <- resources.source_file(source_name)
+      if Path.is_wellformed(name)
+    }
     yield {
+      val file = Path.explode(name).file
       val opt_text =
-        try { Some(File.read(Path.explode(name))) } // FIXME content from resources/models
+        try { Some(File.read(file)) } // FIXME content from resources/models
         catch { case ERROR(_) => None }
-      Line.Node_Range(Url.platform_file(name),
+      Line.Node_Range(Url.print_file(file),
         opt_text match {
           case Some(text) if range.start > 0 =>
             val chunk = Symbol.Text_Chunk(text)
diff -r 1ddc262514b8 -r dd3797f1e0d6 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Tue Jan 03 23:21:09 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Wed Jan 04 12:03:45 2017 +0100
@@ -50,8 +50,7 @@
   override def append(dir: String, source_path: Path): String =
   {
     val path = source_path.expand
-    if (path.is_absolute) Url.platform_file(path)
-    else if (dir == "") Url.platform_file(File.pwd() + path)
+    if (dir == "" || path.is_absolute) Url.print_file(path.file)
     else if (path.is_current) dir
     else Url.normalize_file(dir + "/" + path.implode)
   }
@@ -65,7 +64,7 @@
         f(reader)
 
       case None =>
-        val file = Url.file(uri)
+        val file = Url.parse_file(uri)
         if (!file.isFile) error("No such file: " + quote(file.toString))
 
         val reader = Scan.byte_reader(file)
@@ -133,7 +132,7 @@
             uri = dep.name.node
             if !st.models.isDefinedAt(uri)
             text <-
-              try { Some(File.read(Url.file(uri))) }
+              try { Some(File.read(Url.parse_file(uri))) }
               catch { case ERROR(_) => None }
           }
           yield {