# HG changeset patch
# User wenzelm
# Date 1483267647 -3600
# Node ID 76996d9158940963a616282bc9a9f7ae78430f81
# Parent  4eccd9bc5fd976a5f941494e3f4dd79f19ce0140
clarified modules;

diff -r 4eccd9bc5fd9 -r 76996d915894 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Sun Jan 01 11:38:29 2017 +0100
+++ b/src/Pure/General/file.scala	Sun Jan 01 11:47:27 2017 +0100
@@ -95,22 +95,6 @@
   def platform_path(path: Path): String = platform_path(standard_path(path))
   def platform_file(path: Path): JFile = new JFile(platform_path(path))
 
-  def platform_url(raw_path: Path): String =
-  {
-    val path = raw_path.expand
-    require(path.is_absolute)
-    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 4eccd9bc5fd9 -r 76996d915894 src/Pure/General/url.scala
--- a/src/Pure/General/url.scala	Sun Jan 01 11:38:29 2017 +0100
+++ b/src/Pure/General/url.scala	Sun Jan 01 11:47:27 2017 +0100
@@ -56,4 +56,20 @@
   def is_wellformed_file(uri: String): Boolean =
     try { file(uri); true }
     catch { case _: URISyntaxException | _: IllegalArgumentException => false }
+
+  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")
+      if (!Platform.is_windows) "file://" + s
+      else if (s.startsWith("\\\\")) "file:" + s.replace('\\', '/')
+      else "file:///" + s.replace('\\', '/')
+    }
 }
diff -r 4eccd9bc5fd9 -r 76996d915894 src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Sun Jan 01 11:38:29 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Sun Jan 01 11:47:27 2017 +0100
@@ -84,7 +84,7 @@
       val opt_text =
         try { Some(File.read(Path.explode(name))) } // FIXME content from resources/models
         catch { case ERROR(_) => None }
-      Line.Node_Range(File.platform_url(name),
+      Line.Node_Range(Url.platform_file(name),
         opt_text match {
           case Some(text) if range.start > 0 =>
             val chunk = Symbol.Text_Chunk(text)
diff -r 4eccd9bc5fd9 -r 76996d915894 src/Tools/jEdit/src/jedit_lib.scala
--- a/src/Tools/jEdit/src/jedit_lib.scala	Sun Jan 01 11:38:29 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Sun Jan 01 11:47:27 2017 +0100
@@ -320,7 +320,7 @@
   {
     val name1 =
       if (name.startsWith("idea-icons/")) {
-        val file = File.platform_url(Path.explode("$JEDIT_HOME/dist/jars/idea-icons.jar"))
+        val file = Url.platform_file(Path.explode("$JEDIT_HOME/dist/jars/idea-icons.jar"))
         "jar:" + file + "!/" + name
       }
       else name