# HG changeset patch
# User wenzelm
# Date 1624884213 -7200
# Node ID eb7655fcb090a6554b14d0df000de1da7c7a3667
# Parent  2847a3deedf9e3bec207eb2e89193229c731688d
clarified modules;

diff -r 2847a3deedf9 -r eb7655fcb090 src/Pure/System/cygwin.scala
--- a/src/Pure/System/cygwin.scala	Mon Jun 28 14:24:50 2021 +0200
+++ b/src/Pure/System/cygwin.scala	Mon Jun 28 14:43:33 2021 +0200
@@ -15,51 +15,4 @@
 
 object Cygwin
 {
-  /* init (e.g. after extraction via 7zip) */
-
-  def init(isabelle_root: String, cygwin_root: String): Unit =
-  {
-    require(Platform.is_windows, "Windows platform expected")
-
-    def exec(cmdline: String*): Unit =
-    {
-      val cwd = new JFile(isabelle_root)
-      val env = sys.env + ("CYGWIN" -> "nodosfilewarning")
-      val proc = Isabelle_Env.process(cmdline.toList, cwd = cwd, env = env, redirect = true)
-      val (output, rc) = Isabelle_Env.process_output(proc)
-      if (rc != 0) error(output)
-    }
-
-    val uninitialized_file = new JFile(cygwin_root, "isabelle\\uninitialized")
-    val uninitialized = uninitialized_file.isFile && uninitialized_file.delete
-
-    if (uninitialized) {
-      val symlinks =
-      {
-        val path = (new JFile(cygwin_root + "\\isabelle\\symlinks")).toPath
-        Files.readAllLines(path, UTF8.charset).toArray.toList.asInstanceOf[List[String]]
-      }
-      @tailrec def recover_symlinks(list: List[String]): Unit =
-      {
-        list match {
-          case Nil | List("") =>
-          case target :: content :: rest =>
-            link(content, new JFile(isabelle_root, target))
-            recover_symlinks(rest)
-          case _ => error("Unbalanced symlinks list")
-        }
-      }
-      recover_symlinks(symlinks)
-
-      exec(cygwin_root + "\\bin\\dash.exe", "/isabelle/rebaseall")
-      exec(cygwin_root + "\\bin\\bash.exe", "/isabelle/postinstall")
-    }
-  }
-
-  def link(content: String, target: JFile): Unit =
-  {
-    val target_path = target.toPath
-    Files.writeString(target_path, "!<symlink>" + content + "\u0000")
-    Files.setAttribute(target_path, "dos:system", true)
-  }
 }
diff -r 2847a3deedf9 -r eb7655fcb090 src/Pure/System/isabelle_env.scala
--- a/src/Pure/System/isabelle_env.scala	Mon Jun 28 14:24:50 2021 +0200
+++ b/src/Pure/System/isabelle_env.scala	Mon Jun 28 14:43:33 2021 +0200
@@ -9,9 +9,10 @@
 
 
 import java.io.{File => JFile}
+import java.nio.file.Files
 
 import scala.jdk.CollectionConverters._
-
+import scala.annotation.tailrec
 
 
 object Isabelle_Env
@@ -43,6 +44,61 @@
 
 
 
+  /** Support for Cygwin as POSIX emulation on Windows **/
+
+  /* symlink emulation */
+
+  def cygwin_link(content: String, target: JFile): Unit =
+  {
+    val target_path = target.toPath
+    Files.writeString(target_path, "!<symlink>" + content + "\u0000")
+    Files.setAttribute(target_path, "dos:system", true)
+  }
+
+
+  /* init (e.g. after extraction via 7zip) */
+
+  def cygwin_init(isabelle_root: String, cygwin_root: String): Unit =
+  {
+    require(Platform.is_windows, "Windows platform expected")
+
+    def exec(cmdline: String*): Unit =
+    {
+      val cwd = new JFile(isabelle_root)
+      val env = sys.env + ("CYGWIN" -> "nodosfilewarning")
+      val proc = Isabelle_Env.process(cmdline.toList, cwd = cwd, env = env, redirect = true)
+      val (output, rc) = Isabelle_Env.process_output(proc)
+      if (rc != 0) error(output)
+    }
+
+    val uninitialized_file = new JFile(cygwin_root, "isabelle\\uninitialized")
+    val uninitialized = uninitialized_file.isFile && uninitialized_file.delete
+
+    if (uninitialized) {
+      val symlinks =
+      {
+        val path = (new JFile(cygwin_root + "\\isabelle\\symlinks")).toPath
+        Files.readAllLines(path, UTF8.charset).toArray.toList.asInstanceOf[List[String]]
+      }
+      @tailrec def recover_symlinks(list: List[String]): Unit =
+      {
+        list match {
+          case Nil | List("") =>
+          case target :: content :: rest =>
+            cygwin_link(content, new JFile(isabelle_root, target))
+            recover_symlinks(rest)
+          case _ => error("Unbalanced symlinks list")
+        }
+      }
+      recover_symlinks(symlinks)
+
+      exec(cygwin_root + "\\bin\\dash.exe", "/isabelle/rebaseall")
+      exec(cygwin_root + "\\bin\\bash.exe", "/isabelle/postinstall")
+    }
+  }
+
+
+
   /** raw process **/
 
   /* raw process */
@@ -106,7 +162,7 @@
           bootstrap_directory(cygwin_root, "CYGWIN_ROOT", "cygwin.root", "Cygwin root")
         else ""
 
-      if (Platform.is_windows) Cygwin.init(isabelle_root1, cygwin_root1)
+      if (Platform.is_windows) cygwin_init(isabelle_root1, cygwin_root1)
 
       def set_cygwin_root(): Unit =
       {
diff -r 2847a3deedf9 -r eb7655fcb090 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Mon Jun 28 14:24:50 2021 +0200
+++ b/src/Pure/System/isabelle_system.scala	Mon Jun 28 14:43:33 2021 +0200
@@ -251,12 +251,13 @@
 
     if (force) target.delete
 
+    def cygwin_link(): Unit =
+      Isabelle_Env.cygwin_link(File.standard_path(src), target)
+
     try { Files.createSymbolicLink(target.toPath, src_file.toPath) }
     catch {
-      case _: UnsupportedOperationException if Platform.is_windows =>
-        Cygwin.link(File.standard_path(src), target)
-      case _: FileSystemException if Platform.is_windows =>
-        Cygwin.link(File.standard_path(src), target)
+      case _: UnsupportedOperationException if Platform.is_windows => cygwin_link()
+      case _: FileSystemException if Platform.is_windows => cygwin_link()
     }
   }
 
diff -r 2847a3deedf9 -r eb7655fcb090 src/Pure/build-jars
--- a/src/Pure/build-jars	Mon Jun 28 14:24:50 2021 +0200
+++ b/src/Pure/build-jars	Mon Jun 28 14:43:33 2021 +0200
@@ -133,7 +133,6 @@
   src/Pure/System/bash.scala
   src/Pure/System/command_line.scala
   src/Pure/System/components.scala
-  src/Pure/System/cygwin.scala
   src/Pure/System/executable.scala
   src/Pure/System/getopts.scala
   src/Pure/System/isabelle_charset.scala