# HG changeset patch
# User wenzelm
# Date 1544040918 -3600
# Node ID 61f4c406d7277cb3d73e924969f560ae39531d56
# Parent  7a1b7b737c0283f99e906a16551c8274b4aefb2a
more direct File.link operation: avoid external process;

diff -r 7a1b7b737c02 -r 61f4c406d727 src/Pure/Admin/build_jdk.scala
--- a/src/Pure/Admin/build_jdk.scala	Wed Dec 05 19:42:40 2018 +0100
+++ b/src/Pure/Admin/build_jdk.scala	Wed Dec 05 21:15:18 2018 +0100
@@ -120,8 +120,7 @@
       val platform_dir = dir + Path.explode(platform.name)
       if (platform_dir.is_dir) error("Directory already exists: " + platform_dir)
 
-      val jre_path = jdk_dir + Path.explode(platform.home) + Path.explode("jre")
-      Isabelle_System.bash("ln -s . " + File.bash_path(jre_path)).check
+      File.link(Path.current, jdk_dir + Path.explode(platform.home) + Path.explode("jre"))
 
       File.move(jdk_dir, platform_dir)
 
diff -r 7a1b7b737c02 -r 61f4c406d727 src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Wed Dec 05 19:42:40 2018 +0100
+++ b/src/Pure/Admin/build_release.scala	Wed Dec 05 21:15:18 2018 +0100
@@ -569,9 +569,10 @@
           progress.echo("Application for " + platform)
 
           if (platform == "linux") {
-            Isabelle_System.bash(
-              "ln -s " + Bash.string(isabelle_name + "_linux.tar.gz") + " " +
-              File.bash_path(release.dist_dir + Path.explode(isabelle_name + "_app.tar.gz"))).check
+            File.link(
+              Path.explode(isabelle_name + "_linux.tar.gz"),
+              release.dist_dir + Path.explode(isabelle_name + "_app.tar.gz"),
+              force = true)
           }
           else if (platform == "macos") {
             val dmg_dir = tmp_dir + Path.explode("macos_app/dmg")
@@ -589,21 +590,27 @@
                   terminate_lines(java_options.map(opt => "<string>" + opt + "</string>"))))
 
             for (cp <- classpath) {
-              Isabelle_System.bash(
-                "ln -sf " +
-                Bash.string("../Resources/" + isabelle_name + "/") + File.bash_path(cp) + " " +
-                File.bash_path(app_contents + Path.explode("Java"))).check
+              File.link(
+                Path.explode("../Resources/" + isabelle_name + "/") + cp,
+                app_contents + Path.explode("Java"),
+                force = true)
             }
 
-            Isabelle_System.bash("ln -sf ../Resources/" + Bash.string(isabelle_name) +
-              "/contrib/" + Bash.string(jdk_component) + "/x86_64-darwin " +
-              File.bash_path(app_contents + Path.explode("PlugIns/bundled.jdk"))).check
+            File.link(
+              Path.explode("../Resources/" + isabelle_name + "/contrib/" +
+                jdk_component + "/x86_64-darwin"),
+              app_contents + Path.explode("PlugIns/bundled.jdk"),
+              force = true)
 
-            Isabelle_System.bash("ln -sf ../../Info.plist " +
-              File.bash_path(app_resources + Path.explode(isabelle_name) +
-                Path.explode(isabelle_name + ".plist"))).check
-            Isabelle_System.bash("ln -sf Contents/Resources/" + Bash.string(isabelle_name) + " " +
-              File.bash_path(app_dir) + "/Isabelle").check
+            File.link(
+              Path.explode("../../Info.plist"),
+              app_resources + Path.explode(isabelle_name + "/" + isabelle_name + ".plist"),
+              force = true)
+
+            File.link(
+              Path.explode("Contents/Resources/" + isabelle_name),
+              app_dir + Path.explode("Isabelle"),
+              force = true)
 
             val dmg = Path.explode(isabelle_name + ".dmg")
             (release.dist_dir + dmg).file.delete
diff -r 7a1b7b737c02 -r 61f4c406d727 src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Wed Dec 05 19:42:40 2018 +0100
+++ b/src/Pure/General/file.scala	Wed Dec 05 21:15:18 2018 +0100
@@ -11,7 +11,7 @@
   OutputStream, InputStream, FileInputStream, BufferedInputStream, BufferedReader,
   InputStreamReader, File => JFile, IOException}
 import java.nio.file.{StandardOpenOption, StandardCopyOption, Path => JPath,
-  Files, SimpleFileVisitor, FileVisitOption, FileVisitResult}
+  Files, SimpleFileVisitor, FileVisitOption, FileVisitResult, FileSystemException}
 import java.nio.file.attribute.BasicFileAttributes
 import java.net.{URL, MalformedURLException}
 import java.util.zip.{GZIPInputStream, GZIPOutputStream}
@@ -311,4 +311,24 @@
   }
 
   def move(path1: Path, path2: Path): Unit = move(path1.file, path2.file)
+
+
+  /* symbolic link */
+
+  def link(src: Path, dst: Path, force: Boolean = false)
+  {
+    val src_file = src.file
+    val dst_file = dst.file
+    val target = if (dst_file.isDirectory) new JFile(dst_file, src_file.getName) else dst_file
+
+    if (force) target.delete
+
+    try { Files.createSymbolicLink(target.toPath, src_file.toPath) }
+    catch {
+      case _: UnsupportedOperationException if Platform.is_windows =>
+        Cygwin.link(standard_path(src), target)
+      case _: FileSystemException if Platform.is_windows =>
+        Cygwin.link(standard_path(src), target)
+    }
+  }
 }
diff -r 7a1b7b737c02 -r 61f4c406d727 src/Pure/System/cygwin.scala
--- a/src/Pure/System/cygwin.scala	Wed Dec 05 19:42:40 2018 +0100
+++ b/src/Pure/System/cygwin.scala	Wed Dec 05 21:15:18 2018 +0100
@@ -43,14 +43,8 @@
       {
         list match {
           case Nil | List("") =>
-          case link :: content :: rest =>
-            val path = (new JFile(isabelle_root, link)).toPath
-
-            using(Files.newBufferedWriter(path, UTF8.charset))(
-              _.write("!<symlink>" + content + "\u0000"))
-
-            Files.setAttribute(path, "dos:system", true)
-
+          case target :: content :: rest =>
+            link(content, new JFile(isabelle_root, target))
             recover_symlinks(rest)
           case _ => error("Unbalanced symlinks list")
         }
@@ -61,4 +55,14 @@
       exec(cygwin_root + "\\bin\\bash.exe", "/isabelle/postinstall")
     }
   }
+
+  def link(content: String, target: JFile)
+  {
+    val target_path = target.toPath
+
+    using(Files.newBufferedWriter(target_path, UTF8.charset))(
+      _.write("!<symlink>" + content + "\u0000"))
+
+    Files.setAttribute(target_path, "dos:system", true)
+  }
 }