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