support for native symlinks on Windows;
authorwenzelm
Tue, 27 Jul 2021 13:12:27 +0200
changeset 74335 a69a13c4b049
parent 74332 62e4ec8cff38
child 74336 b25b7c264a93
support for native symlinks on Windows;
src/Pure/System/isabelle_system.scala
src/Pure/Tools/scala_project.scala
--- a/src/Pure/System/isabelle_system.scala	Mon Jul 26 13:12:22 2021 +0200
+++ b/src/Pure/System/isabelle_system.scala	Tue Jul 27 13:12:27 2021 +0200
@@ -253,7 +253,7 @@
 
   /* symbolic link */
 
-  def symlink(src: Path, dst: Path, force: Boolean = false): Unit =
+  def symlink(src: Path, dst: Path, force: Boolean = false, native: Boolean = false): Unit =
   {
     val src_file = src.file
     val dst_file = dst.file
@@ -262,7 +262,14 @@
     if (force) target.delete
 
     def cygwin_link(): Unit =
-      isabelle.setup.Environment.cygwin_link(File.standard_path(src), target)
+    {
+      if (native) {
+        error("Failed to create native symlink on Windows: " + quote(src_file.toString) +
+          "\n(but it could work as Administrator)")
+      }
+      else isabelle.setup.Environment.cygwin_link(File.standard_path(src), target)
+    }
+
 
     try { Files.createSymbolicLink(target.toPath, src_file.toPath) }
     catch {
--- a/src/Pure/Tools/scala_project.scala	Mon Jul 26 13:12:22 2021 +0200
+++ b/src/Pure/Tools/scala_project.scala	Tue Jul 27 13:12:27 2021 +0200
@@ -109,9 +109,6 @@
 
   def scala_project(project_dir: Path, symlinks: Boolean = false): Unit =
   {
-    if (symlinks && Platform.is_windows)
-      error("Cannot create symlinks on Windows")
-
     if (project_dir.is_file || project_dir.is_dir)
       error("Project directory already exists: " + project_dir)
 
@@ -125,7 +122,7 @@
       val dir = if (source.is_java) java_src_dir else scala_src_dir
       val target = dir + the_package_dir(source)
       Isabelle_System.make_directory(target)
-      if (symlinks) Isabelle_System.symlink(source, target)
+      if (symlinks) Isabelle_System.symlink(source, target, native = true)
       else Isabelle_System.copy_file(source, target)
     }