# HG changeset patch
# User wenzelm
# Date 1498825177 -7200
# Node ID 836898197296c15c9f9c1aabf601c3a8f97675cd
# Parent  7188967253e57a7b09d1359da273278e50b849f3
clarified platform file operations;

diff -r 7188967253e5 -r 836898197296 src/Pure/General/url.scala
--- a/src/Pure/General/url.scala	Fri Jun 30 14:17:48 2017 +0200
+++ b/src/Pure/General/url.scala	Fri Jun 30 14:19:37 2017 +0200
@@ -49,7 +49,7 @@
 
   /* file URIs */
 
-  def print_file(file: JFile): String = file.toPath.toAbsolutePath.toUri.normalize.toString
+  def print_file(file: JFile): String = File.absolute(file).toPath.toUri.toString
   def print_file_name(name: String): String = print_file(new JFile(name))
 
   def parse_file(uri: String): JFile = Paths.get(new URI(uri)).toFile
@@ -61,6 +61,6 @@
         false
     }
 
-  def canonical_file(uri: String): JFile = parse_file(uri).getCanonicalFile
+  def canonical_file(uri: String): JFile = File.canonical(parse_file(uri))
   def canonical_file_name(uri: String): String = canonical_file(uri).getPath
 }
diff -r 7188967253e5 -r 836898197296 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri Jun 30 14:17:48 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Fri Jun 30 14:19:37 2017 +0200
@@ -83,7 +83,7 @@
 
     def get_file(file: JFile, bootstrap: Boolean = false): Option[Document.Node.Name] =
     {
-      val res = files.getOrElse(file.getCanonicalFile, Nil).headOption
+      val res = files.getOrElse(File.canonical(file), Nil).headOption
       if (bootstrap) res.map(_.map_theory(Thy_Header.bootstrap_name(_))) else res
     }
   }
diff -r 7188967253e5 -r 836898197296 src/Pure/Tools/imports.scala
--- a/src/Pure/Tools/imports.scala	Fri Jun 30 14:17:48 2017 +0200
+++ b/src/Pure/Tools/imports.scala	Fri Jun 30 14:19:37 2017 +0200
@@ -25,7 +25,7 @@
         for {
           name <- hg.known_files()
           file = (hg.root + Path.explode(name)).file
-          if pred(file) && file.getCanonicalFile.toPath.startsWith(start_path)
+          if pred(file) && File.canonical(file).toPath.startsWith(start_path)
         } yield file
     }
 
diff -r 7188967253e5 -r 836898197296 src/Tools/VSCode/src/vscode_rendering.scala
--- a/src/Tools/VSCode/src/vscode_rendering.scala	Fri Jun 30 14:17:48 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_rendering.scala	Fri Jun 30 14:19:37 2017 +0200
@@ -254,7 +254,7 @@
     for {
       platform_path <- resources.source_file(source_name)
       file <-
-        (try { Some(new JFile(platform_path).getCanonicalFile) }
+        (try { Some(File.canonical(new JFile(platform_path))) }
          catch { case ERROR(_) => None })
     }
     yield {
diff -r 7188967253e5 -r 836898197296 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Fri Jun 30 14:17:48 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Fri Jun 30 14:19:37 2017 +0200
@@ -109,7 +109,7 @@
     else if (path.is_basic && !dir.endsWith("/") && !dir.endsWith(JFile.separator))
       dir + JFile.separator + File.platform_path(path)
     else if (path.is_basic) dir + File.platform_path(path)
-    else new JFile(dir + JFile.separator + File.platform_path(path)).getCanonicalPath
+    else File.canonical_name(new JFile(dir + JFile.separator + File.platform_path(path)))
   }
 
   def get_models: Map[JFile, Document_Model] = state.value.models
diff -r 7188967253e5 -r 836898197296 src/Tools/jEdit/src/scala_console.scala
--- a/src/Tools/jEdit/src/scala_console.scala	Fri Jun 30 14:17:48 2017 +0200
+++ b/src/Tools/jEdit/src/scala_console.scala	Fri Jun 30 14:19:37 2017 +0200
@@ -30,7 +30,7 @@
     def find_jars(start: String): List[String] =
       if (start != null)
         File.find_files(new JFile(start), file => file.getName.endsWith(".jar")).
-          map(_.getAbsolutePath)
+          map(File.absolute_name(_))
       else Nil
 
     val initial_class_path =