diff --git a/src/Pure/Admin/build_cygwin.scala b/src/Pure/Admin/build_cygwin.scala
--- a/src/Pure/Admin/build_cygwin.scala
+++ b/src/Pure/Admin/build_cygwin.scala
@@ -1,89 +1,89 @@
 /*  Title:      Pure/Admin/build_cygwin.scala
     Author:     Makarius
 
 Produce pre-canned Cygwin distribution for Isabelle.
 */
 
 package isabelle
 
 
 object Build_Cygwin
 {
   val default_mirror: String = "https://isabelle.sketis.net/cygwin_2020"
 
   val packages: List[String] =
     List("curl", "libgmp-devel", "nano", "perl", "perl-libwww-perl", "rlwrap", "unzip")
 
   def build_cygwin(progress: Progress,
     mirror: String = default_mirror,
     more_packages: List[String] = Nil)
   {
     require(Platform.is_windows)
 
     Isabelle_System.with_tmp_dir("cygwin")(tmp_dir =>
       {
         val cygwin = tmp_dir + Path.explode("cygwin")
         val cygwin_etc = cygwin + Path.explode("etc")
         val cygwin_isabelle = cygwin + Path.explode("isabelle")
         Isabelle_System.mkdirs(cygwin_isabelle)
 
         val cygwin_exe_name = mirror + "/setup-x86_64.exe"
         val cygwin_exe = cygwin_isabelle + Path.explode("cygwin.exe")
         Bytes.write(cygwin_exe,
           try { Bytes.read(Url(cygwin_exe_name)) }
           catch { case ERROR(_) => error("Failed to download " + quote(cygwin_exe_name)) })
 
         File.write(cygwin_isabelle + Path.explode("cygwin_mirror"), mirror)
 
         File.set_executable(cygwin_exe, true)
         Isabelle_System.bash(File.bash_path(cygwin_exe) + " -h </dev/null >/dev/null").check
 
         val res =
           progress.bash(
             File.bash_path(cygwin_exe) + " --site " + Bash.string(mirror) + " --no-verify" +
               " --local-package-dir 'C:\\temp'" +
-              " --root " + Bash.string(File.platform_path(cygwin)) +
+              " --root " + File.bash_platform_path(cygwin) +
               " --packages " + quote((packages ::: more_packages).mkString(",")) +
               " --no-shortcuts --no-startmenu --no-desktop --quiet-mode",
             echo = true)
         if (!res.ok || !cygwin_etc.is_dir) error("Failed")
 
         for (name <- List("hosts", "protocols", "services", "networks", "passwd", "group"))
           (cygwin_etc + Path.explode(name)).file.delete
 
         (cygwin + Path.explode("Cygwin.bat")).file.delete
 
         val archive = "cygwin-" + Date.Format("uuuuMMdd")(Date.now()) + ".tar.gz"
         Isabelle_System.gnutar("-czf " + Bash.string(archive) + " cygwin", dir = tmp_dir).check
       })
   }
 
 
   /* Isabelle tool wrapper */
 
   val isabelle_tool =
     Isabelle_Tool("build_cygwin", "produce pre-canned Cygwin distribution for Isabelle", args =>
     {
       var mirror = default_mirror
       var more_packages: List[String] = Nil
 
       val getopts =
         Getopts("""
 Usage: isabelle build_cygwin [OPTIONS]
 
   Options are:
     -R MIRROR    Cygwin mirror site (default """ + quote(default_mirror) + """)
     -p NAME      additional Cygwin package
 
   Produce pre-canned Cygwin distribution for Isabelle: this requires
   Windows administrator mode.
 """,
           "R:" -> (arg => mirror = arg),
           "p:" -> (arg => more_packages ::= arg))
 
       val more_args = getopts(args)
       if (more_args.nonEmpty) getopts.usage()
 
       build_cygwin(new Console_Progress(), mirror = mirror, more_packages = more_packages)
     })
 }
diff --git a/src/Pure/General/file.scala b/src/Pure/General/file.scala
--- a/src/Pure/General/file.scala
+++ b/src/Pure/General/file.scala
@@ -1,358 +1,360 @@
 /*  Title:      Pure/General/file.scala
     Author:     Makarius
 
 File-system operations.
 */
 
 package isabelle
 
 
 import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream, BufferedOutputStream,
   OutputStream, InputStream, FileInputStream, BufferedInputStream, BufferedReader,
   InputStreamReader, File => JFile, IOException}
 import java.nio.file.{StandardOpenOption, StandardCopyOption, Path => JPath,
   Files, SimpleFileVisitor, FileVisitOption, FileVisitResult, FileSystemException}
 import java.nio.file.attribute.BasicFileAttributes
 import java.net.{URL, MalformedURLException}
 import java.util.zip.{GZIPInputStream, GZIPOutputStream}
 import java.util.regex.Pattern
 import java.util.EnumSet
 
 import org.tukaani.xz.{XZInputStream, XZOutputStream}
 
 import scala.collection.mutable
 import scala.util.matching.Regex
 
 
 object File
 {
   /* standard path (Cygwin or Posix) */
 
   def standard_path(path: Path): String = path.expand.implode
 
   def standard_path(platform_path: String): String =
     if (Platform.is_windows) {
       val Platform_Root = new Regex("(?i)" +
         Pattern.quote(Isabelle_System.cygwin_root()) + """(?:\\+|\z)(.*)""")
       val Drive = new Regex("""([a-zA-Z]):\\*(.*)""")
 
       platform_path.replace('/', '\\') match {
         case Platform_Root(rest) => "/" + rest.replace('\\', '/')
         case Drive(letter, rest) =>
           "/cygdrive/" + Word.lowercase(letter) +
             (if (rest == "") "" else "/" + rest.replace('\\', '/'))
         case path => path.replace('\\', '/')
       }
     }
     else platform_path
 
   def standard_path(file: JFile): String = standard_path(file.getPath)
 
   def standard_url(name: String): String =
     try {
       val url = new URL(name)
       if (url.getProtocol == "file" && Url.is_wellformed_file(name))
         standard_path(Url.parse_file(name))
       else name
     }
     catch { case _: MalformedURLException => standard_path(name) }
 
 
   /* platform path (Windows or Posix) */
 
   private val Cygdrive = new Regex("/cygdrive/([a-zA-Z])($|/.*)")
   private val Named_Root = new Regex("//+([^/]*)(.*)")
 
   def platform_path(standard_path: String): String =
     if (Platform.is_windows) {
       val result_path = new StringBuilder
       val rest =
         standard_path match {
           case Cygdrive(drive, rest) =>
             result_path ++= (Word.uppercase(drive) + ":" + JFile.separator)
             rest
           case Named_Root(root, rest) =>
             result_path ++= JFile.separator
             result_path ++= JFile.separator
             result_path ++= root
             rest
           case path if path.startsWith("/") =>
             result_path ++= Isabelle_System.cygwin_root()
             path
           case path => path
         }
       for (p <- space_explode('/', rest) if p != "") {
         val len = result_path.length
         if (len > 0 && result_path(len - 1) != JFile.separatorChar)
           result_path += JFile.separatorChar
         result_path ++= p
       }
       result_path.toString
     }
     else standard_path
 
   def platform_path(path: Path): String = platform_path(standard_path(path))
   def platform_file(path: Path): JFile = new JFile(platform_path(path))
 
 
   /* platform files */
 
   def absolute(file: JFile): JFile = file.toPath.toAbsolutePath.normalize.toFile
   def absolute_name(file: JFile): String = absolute(file).getPath
 
   def canonical(file: JFile): JFile = file.getCanonicalFile
   def canonical_name(file: JFile): String = canonical(file).getPath
 
   def path(file: JFile): Path = Path.explode(standard_path(file))
   def pwd(): Path = path(Path.current.absolute_file)
 
 
   /* relative paths */
 
   def relative_path(base: Path, other: Path): Option[Path] =
   {
     val base_path = base.file.toPath
     val other_path = other.file.toPath
     if (other_path.startsWith(base_path))
       Some(path(base_path.relativize(other_path).toFile))
     else None
   }
 
 
   /* bash path */
 
   def bash_path(path: Path): String = Bash.string(standard_path(path))
   def bash_path(file: JFile): String = Bash.string(standard_path(file))
 
+  def bash_platform_path(path: Path): String = Bash.string(platform_path(path))
+
 
   /* directory entries */
 
   def check_dir(path: Path): Path =
     if (path.is_dir) path else error("No such directory: " + path)
 
   def check_file(path: Path): Path =
     if (path.is_file) path else error("No such file: " + path)
 
 
   /* directory content */
 
   def read_dir(dir: Path): List[String] =
   {
     if (!dir.is_dir) error("No such directory: " + dir.toString)
     val files = dir.file.listFiles
     if (files == null) Nil
     else files.toList.map(_.getName).sorted
   }
 
   def find_files(
     start: JFile,
     pred: JFile => Boolean = _ => true,
     include_dirs: Boolean = false,
     follow_links: Boolean = false): List[JFile] =
   {
     val result = new mutable.ListBuffer[JFile]
     def check(file: JFile) { if (pred(file)) result += file }
 
     if (start.isFile) check(start)
     else if (start.isDirectory) {
       val options =
         if (follow_links) EnumSet.of(FileVisitOption.FOLLOW_LINKS)
         else EnumSet.noneOf(classOf[FileVisitOption])
       Files.walkFileTree(start.toPath, options, Integer.MAX_VALUE,
         new SimpleFileVisitor[JPath] {
           override def preVisitDirectory(path: JPath, attrs: BasicFileAttributes): FileVisitResult =
           {
             if (include_dirs) check(path.toFile)
             FileVisitResult.CONTINUE
           }
           override def visitFile(path: JPath, attrs: BasicFileAttributes): FileVisitResult =
           {
             val file = path.toFile
             if (include_dirs || !file.isDirectory) check(file)
             FileVisitResult.CONTINUE
           }
         }
       )
     }
 
     result.toList
   }
 
 
   /* read */
 
   def read(file: JFile): String = Bytes.read(file).text
   def read(path: Path): String = read(path.file)
 
 
   def read_stream(reader: BufferedReader): String =
   {
     val output = new StringBuilder(100)
     var c = -1
     while ({ c = reader.read; c != -1 }) output += c.toChar
     reader.close
     output.toString
   }
 
   def read_stream(stream: InputStream): String =
     read_stream(new BufferedReader(new InputStreamReader(stream, UTF8.charset)))
 
   def read_gzip(file: JFile): String =
     read_stream(new GZIPInputStream(new BufferedInputStream(new FileInputStream(file))))
   def read_gzip(path: Path): String = read_gzip(path.file)
 
   def read_xz(file: JFile): String =
     read_stream(new XZInputStream(new BufferedInputStream(new FileInputStream(file))))
   def read_xz(path: Path): String = read_xz(path.file)
 
 
   /* read lines */
 
   def read_line(reader: BufferedReader): Option[String] =
   {
     val line =
       try { reader.readLine}
       catch { case _: IOException => null }
     Option(line)
   }
 
   def read_lines(reader: BufferedReader, progress: String => Unit): List[String] =
   {
     val result = new mutable.ListBuffer[String]
     var line: Option[String] = None
     while ({ line = read_line(reader); line.isDefined }) {
       progress(line.get)
       result += line.get
     }
     reader.close
     result.toList
   }
 
 
   /* write */
 
   def writer(file: JFile): BufferedWriter =
     new BufferedWriter(new OutputStreamWriter(new FileOutputStream(file), UTF8.charset))
 
   def write_file(file: JFile, text: CharSequence, make_stream: OutputStream => OutputStream)
   {
     val stream = make_stream(new FileOutputStream(file))
     using(new BufferedWriter(new OutputStreamWriter(stream, UTF8.charset)))(_.append(text))
   }
 
   def write(file: JFile, text: CharSequence): Unit = write_file(file, text, s => s)
   def write(path: Path, text: CharSequence): Unit = write(path.file, text)
 
   def write_gzip(file: JFile, text: CharSequence): Unit =
     write_file(file, text, (s: OutputStream) => new GZIPOutputStream(new BufferedOutputStream(s)))
   def write_gzip(path: Path, text: CharSequence): Unit = write_gzip(path.file, text)
 
   def write_xz(file: JFile, text: CharSequence, options: XZ.Options): Unit =
     File.write_file(file, text, s => new XZOutputStream(new BufferedOutputStream(s), options))
   def write_xz(file: JFile, text: CharSequence): Unit = write_xz(file, text, XZ.options())
   def write_xz(path: Path, text: CharSequence, options: XZ.Options): Unit =
     write_xz(path.file, text, options)
   def write_xz(path: Path, text: CharSequence): Unit = write_xz(path, text, XZ.options())
 
   def write_backup(path: Path, text: CharSequence)
   {
     if (path.is_file) move(path, path.backup)
     write(path, text)
   }
 
   def write_backup2(path: Path, text: CharSequence)
   {
     if (path.is_file) move(path, path.backup2)
     write(path, text)
   }
 
 
   /* append */
 
   def append(file: JFile, text: CharSequence): Unit =
     Files.write(file.toPath, UTF8.bytes(text.toString),
       StandardOpenOption.APPEND, StandardOpenOption.CREATE)
 
   def append(path: Path, text: CharSequence): Unit = append(path.file, text)
 
 
   /* eq */
 
   def eq(file1: JFile, file2: JFile): Boolean =
     try { java.nio.file.Files.isSameFile(file1.toPath, file2.toPath) }
     catch { case ERROR(_) => false }
 
   def eq(path1: Path, path2: Path): Boolean = eq(path1.file, path2.file)
 
 
   /* eq_content */
 
   def eq_content(file1: JFile, file2: JFile): Boolean =
     if (eq(file1, file2)) true
     else if (file1.length != file2.length) false
     else Bytes.read(file1) == Bytes.read(file2)
 
   def eq_content(path1: Path, path2: Path): Boolean = eq_content(path1.file, path2.file)
 
 
   /* copy */
 
   def copy(src: JFile, dst: JFile)
   {
     val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst
     if (!eq(src, target))
       Files.copy(src.toPath, target.toPath,
         StandardCopyOption.COPY_ATTRIBUTES,
         StandardCopyOption.REPLACE_EXISTING)
   }
 
   def copy(path1: Path, path2: Path): Unit = copy(path1.file, path2.file)
 
 
   /* move */
 
   def move(src: JFile, dst: JFile)
   {
     val target = if (dst.isDirectory) new JFile(dst, src.getName) else dst
     if (!eq(src, target))
       Files.move(src.toPath, target.toPath, StandardCopyOption.REPLACE_EXISTING)
   }
 
   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)
     }
   }
 
 
   /* permissions */
 
   def is_executable(path: Path): Boolean =
   {
     if (Platform.is_windows) Isabelle_System.bash("test -x " + bash_path(path)).check.ok
     else path.file.canExecute
   }
 
   def set_executable(path: Path, flag: Boolean)
   {
     if (Platform.is_windows && flag) Isabelle_System.chmod("a+x", path)
     else if (Platform.is_windows) Isabelle_System.chmod("a-x", path)
     else path.file.setExecutable(flag, false)
   }
 }