src/Pure/System/cygwin.scala
author wenzelm
Tue Jan 05 13:48:51 2016 +0100 (2016-01-05)
changeset 62058 1cfd5d604937
parent 61293 876e7eae22be
child 62291 98df25a6e2ac
permissions -rw-r--r--
updated headers;
wenzelm@62058
     1
/*  Title:      Pure/System/cygwin.scala
wenzelm@61282
     2
    Author:     Makarius
wenzelm@61282
     3
wenzelm@61282
     4
Cygwin as POSIX emulation on Windows.
wenzelm@61282
     5
*/
wenzelm@61282
     6
wenzelm@61282
     7
package isabelle
wenzelm@61282
     8
wenzelm@61282
     9
wenzelm@61282
    10
import java.io.{File => JFile}
wenzelm@61282
    11
import java.nio.file.Files
wenzelm@61282
    12
wenzelm@61282
    13
import scala.annotation.tailrec
wenzelm@61282
    14
wenzelm@61282
    15
wenzelm@61282
    16
object Cygwin
wenzelm@61282
    17
{
wenzelm@61291
    18
  /* init (e.g. after extraction via 7zip) */
wenzelm@61282
    19
wenzelm@61293
    20
  def init(isabelle_root: String, cygwin_root: String)
wenzelm@61291
    21
  {
wenzelm@61291
    22
    require(Platform.is_windows)
wenzelm@61282
    23
wenzelm@61291
    24
    def execute(args: String*)
wenzelm@61291
    25
    {
wenzelm@61293
    26
      val cwd = new JFile(isabelle_root)
wenzelm@61291
    27
      val env = Map("CYGWIN" -> "nodosfilewarning")
wenzelm@61291
    28
      val proc = Isabelle_System.raw_execute(cwd, env, true, args: _*)
wenzelm@61291
    29
      val (output, rc) = Isabelle_System.process_output(proc)
wenzelm@61291
    30
      if (rc != 0) error(output)
wenzelm@61291
    31
    }
wenzelm@61282
    32
wenzelm@61291
    33
    val uninitialized_file = new JFile(cygwin_root, "isabelle\\uninitialized")
wenzelm@61291
    34
    val uninitialized = uninitialized_file.isFile && uninitialized_file.delete
wenzelm@61282
    35
wenzelm@61291
    36
    if (uninitialized) {
wenzelm@61291
    37
      val symlinks =
wenzelm@61291
    38
      {
wenzelm@61291
    39
        val path = (new JFile(cygwin_root + "\\isabelle\\symlinks")).toPath
wenzelm@61291
    40
        Files.readAllLines(path, UTF8.charset).toArray.toList.asInstanceOf[List[String]]
wenzelm@61291
    41
      }
wenzelm@61291
    42
      @tailrec def recover_symlinks(list: List[String]): Unit =
wenzelm@61291
    43
      {
wenzelm@61291
    44
        list match {
wenzelm@61291
    45
          case Nil | List("") =>
wenzelm@61291
    46
          case link :: content :: rest =>
wenzelm@61293
    47
            val path = (new JFile(isabelle_root, link)).toPath
wenzelm@61282
    48
wenzelm@61291
    49
            val writer = Files.newBufferedWriter(path, UTF8.charset)
wenzelm@61291
    50
            try { writer.write("!<symlink>" + content + "\u0000") }
wenzelm@61291
    51
            finally { writer.close }
wenzelm@61291
    52
wenzelm@61291
    53
            Files.setAttribute(path, "dos:system", true)
wenzelm@61291
    54
wenzelm@61291
    55
            recover_symlinks(rest)
wenzelm@61291
    56
          case _ => error("Unbalanced symlinks list")
wenzelm@61282
    57
        }
wenzelm@61291
    58
      }
wenzelm@61291
    59
      recover_symlinks(symlinks)
wenzelm@61282
    60
wenzelm@61291
    61
      execute(cygwin_root + "\\bin\\dash.exe", "/isabelle/rebaseall")
wenzelm@61291
    62
      execute(cygwin_root + "\\bin\\bash.exe", "/isabelle/postinstall")
wenzelm@61282
    63
    }
wenzelm@61282
    64
  }
wenzelm@61282
    65
}