# HG changeset patch
# User wenzelm
# Date 1627384347 -7200
# Node ID a69a13c4b04923486092877c4245d54a4ab10b41
# Parent  62e4ec8cff387dd40d67568a60e887996610e328
support for native symlinks on Windows;

diff -r 62e4ec8cff38 -r a69a13c4b049 src/Pure/System/isabelle_system.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 {
diff -r 62e4ec8cff38 -r a69a13c4b049 src/Pure/Tools/scala_project.scala
--- 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)
     }