| author | wenzelm | 
| Wed, 27 May 2020 20:02:02 +0200 | |
| changeset 71910 | f8b0271cc744 | 
| parent 69402 | 61f4c406d727 | 
| child 73120 | c3589f2dff31 | 
| 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("") =>
 | |
| 69402 
61f4c406d727
more direct File.link operation: avoid external process;
 wenzelm parents: 
69393diff
changeset | 46 | case target :: content :: rest => | 
| 
61f4c406d727
more direct File.link operation: avoid external process;
 wenzelm parents: 
69393diff
changeset | 47 | link(content, new JFile(isabelle_root, target)) | 
| 61291 | 48 | recover_symlinks(rest) | 
| 49 |           case _ => error("Unbalanced symlinks list")
 | |
| 61282 | 50 | } | 
| 61291 | 51 | } | 
| 52 | recover_symlinks(symlinks) | |
| 61282 | 53 | |
| 62610 
4c89504c76fb
more uniform signature for various process invocations;
 wenzelm parents: 
62291diff
changeset | 54 | exec(cygwin_root + "\\bin\\dash.exe", "/isabelle/rebaseall") | 
| 
4c89504c76fb
more uniform signature for various process invocations;
 wenzelm parents: 
62291diff
changeset | 55 | exec(cygwin_root + "\\bin\\bash.exe", "/isabelle/postinstall") | 
| 61282 | 56 | } | 
| 57 | } | |
| 69402 
61f4c406d727
more direct File.link operation: avoid external process;
 wenzelm parents: 
69393diff
changeset | 58 | |
| 
61f4c406d727
more direct File.link operation: avoid external process;
 wenzelm parents: 
69393diff
changeset | 59 | def link(content: String, target: JFile) | 
| 
61f4c406d727
more direct File.link operation: avoid external process;
 wenzelm parents: 
69393diff
changeset | 60 |   {
 | 
| 
61f4c406d727
more direct File.link operation: avoid external process;
 wenzelm parents: 
69393diff
changeset | 61 | val target_path = target.toPath | 
| 
61f4c406d727
more direct File.link operation: avoid external process;
 wenzelm parents: 
69393diff
changeset | 62 | |
| 
61f4c406d727
more direct File.link operation: avoid external process;
 wenzelm parents: 
69393diff
changeset | 63 | using(Files.newBufferedWriter(target_path, UTF8.charset))( | 
| 
61f4c406d727
more direct File.link operation: avoid external process;
 wenzelm parents: 
69393diff
changeset | 64 |       _.write("!<symlink>" + content + "\u0000"))
 | 
| 
61f4c406d727
more direct File.link operation: avoid external process;
 wenzelm parents: 
69393diff
changeset | 65 | |
| 
61f4c406d727
more direct File.link operation: avoid external process;
 wenzelm parents: 
69393diff
changeset | 66 | Files.setAttribute(target_path, "dos:system", true) | 
| 
61f4c406d727
more direct File.link operation: avoid external process;
 wenzelm parents: 
69393diff
changeset | 67 | } | 
| 61282 | 68 | } |