# HG changeset patch
# User wenzelm
# Date 1482520014 -3600
# Node ID 39a6c88c059b6d431d7ec65fd29daba46523ac57
# Parent  cdb0d559a24b7a5415c96eb21a9c39e2b9cb4520
proper file:// URL for external references;

diff -r cdb0d559a24b -r 39a6c88c059b src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Fri Dec 23 19:19:59 2016 +0100
+++ b/src/Pure/General/file.scala	Fri Dec 23 20:06:54 2016 +0100
@@ -99,12 +99,18 @@
   {
     val path = raw_path.expand
     require(path.is_absolute)
-    val s = platform_path(path).replaceAll(" ", "%20")
-    if (!Platform.is_windows) "file://" + s
-    else if (s.startsWith("\\\\")) "file:" + s.replace('\\', '/')
-    else "file:///" + s.replace('\\', '/')
+    platform_url(platform_path(path))
   }
 
+  def platform_url(name: String): String =
+    if (name.startsWith("file://")) name
+    else {
+      val s = name.replaceAll(" ", "%20")
+      if (!Platform.is_windows) "file://" + s
+      else if (s.startsWith("\\\\")) "file:" + s.replace('\\', '/')
+      else "file:///" + s.replace('\\', '/')
+    }
+
 
   /* bash path */
 
diff -r cdb0d559a24b -r 39a6c88c059b src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Fri Dec 23 19:19:59 2016 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Fri Dec 23 20:06:54 2016 +0100
@@ -40,7 +40,7 @@
       val opt_text =
         try { Some(File.read(Path.explode(name))) } // FIXME content from resources/models
         catch { case ERROR(_) => None }
-      Line.Node_Range(name,
+      Line.Node_Range(File.platform_url(name),
         opt_text match {
           case Some(text) if range.start > 0 =>
             val chunk = Symbol.Text_Chunk(text)