13 import scala.annotation.tailrec |
13 import scala.annotation.tailrec |
14 |
14 |
15 |
15 |
16 object Cygwin |
16 object Cygwin |
17 { |
17 { |
18 /** Cygwin init (e.g. after extraction via 7zip) **/ |
18 /* init (e.g. after extraction via 7zip) */ |
19 |
19 |
20 def init() |
20 def init(isabelle_home: String, cygwin_root: String) |
21 { |
21 { |
22 val isabelle_home0 = System.getenv("ISABELLE_HOME") |
22 require(Platform.is_windows) |
23 if (isabelle_home0 == null || isabelle_home0 == "") { |
|
24 |
23 |
25 /* isabelle_home */ |
24 def execute(args: String*) |
|
25 { |
|
26 val cwd = new JFile(isabelle_home) |
|
27 val env = Map("CYGWIN" -> "nodosfilewarning") |
|
28 val proc = Isabelle_System.raw_execute(cwd, env, true, args: _*) |
|
29 val (output, rc) = Isabelle_System.process_output(proc) |
|
30 if (rc != 0) error(output) |
|
31 } |
26 |
32 |
27 val isabelle_home = System.getProperty("isabelle.home", "") |
33 val uninitialized_file = new JFile(cygwin_root, "isabelle\\uninitialized") |
|
34 val uninitialized = uninitialized_file.isFile && uninitialized_file.delete |
28 |
35 |
29 if (isabelle_home == "") |
36 if (uninitialized) { |
30 error("Unknown Isabelle home directory") |
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 => |
|
47 val path = (new JFile(isabelle_home, link)).toPath |
31 |
48 |
32 if (!(new JFile(isabelle_home)).isDirectory) |
49 val writer = Files.newBufferedWriter(path, UTF8.charset) |
33 error("Bad Isabelle home directory: " + quote(isabelle_home)) |
50 try { writer.write("!<symlink>" + content + "\u0000") } |
|
51 finally { writer.close } |
34 |
52 |
35 def execute(args: String*) |
53 Files.setAttribute(path, "dos:system", true) |
36 { |
54 |
37 val cwd = new JFile(isabelle_home) |
55 recover_symlinks(rest) |
38 val env = Map("CYGWIN" -> "nodosfilewarning") |
56 case _ => error("Unbalanced symlinks list") |
39 val proc = Isabelle_System.raw_execute(cwd, env, true, args: _*) |
57 } |
40 val (output, rc) = Isabelle_System.process_output(proc) |
|
41 if (rc != 0) error(output) |
|
42 } |
58 } |
|
59 recover_symlinks(symlinks) |
43 |
60 |
44 |
61 execute(cygwin_root + "\\bin\\dash.exe", "/isabelle/rebaseall") |
45 /* cygwin_root */ |
62 execute(cygwin_root + "\\bin\\bash.exe", "/isabelle/postinstall") |
46 |
|
47 val cygwin_root = isabelle_home + "\\contrib\\cygwin" |
|
48 if ((new JFile(cygwin_root)).isDirectory) |
|
49 System.setProperty("cygwin.root", cygwin_root) |
|
50 |
|
51 |
|
52 /* init */ |
|
53 |
|
54 val uninitialized_file = new JFile(cygwin_root, "isabelle\\uninitialized") |
|
55 val uninitialized = uninitialized_file.isFile && uninitialized_file.delete |
|
56 |
|
57 if (uninitialized) { |
|
58 val symlinks = |
|
59 { |
|
60 val path = (new JFile(cygwin_root + "\\isabelle\\symlinks")).toPath |
|
61 Files.readAllLines(path, UTF8.charset).toArray.toList.asInstanceOf[List[String]] |
|
62 } |
|
63 @tailrec def recover_symlinks(list: List[String]): Unit = |
|
64 { |
|
65 list match { |
|
66 case Nil | List("") => |
|
67 case link :: content :: rest => |
|
68 val path = (new JFile(isabelle_home, link)).toPath |
|
69 |
|
70 val writer = Files.newBufferedWriter(path, UTF8.charset) |
|
71 try { writer.write("!<symlink>" + content + "\u0000") } |
|
72 finally { writer.close } |
|
73 |
|
74 Files.setAttribute(path, "dos:system", true) |
|
75 |
|
76 recover_symlinks(rest) |
|
77 case _ => error("Unbalanced symlinks list") |
|
78 } |
|
79 } |
|
80 recover_symlinks(symlinks) |
|
81 |
|
82 execute(cygwin_root + "\\bin\\dash.exe", "/isabelle/rebaseall") |
|
83 execute(cygwin_root + "\\bin\\bash.exe", "/isabelle/postinstall") |
|
84 } |
|
85 } |
63 } |
86 } |
64 } |
87 } |
65 } |