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