| author | wenzelm | 
| Fri, 19 Jan 2018 20:09:04 +0100 | |
| changeset 67476 | 44b018d4aa5f | 
| 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: 
61291 
diff
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: 
62291 
diff
changeset
 | 
24  | 
def exec(cmdline: String*)  | 
| 61291 | 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)  | 
| 
62610
 
4c89504c76fb
more uniform signature for various process invocations;
 
wenzelm 
parents: 
62291 
diff
changeset
 | 
27  | 
      val env = sys.env + ("CYGWIN" -> "nodosfilewarning")
 | 
| 
 
4c89504c76fb
more uniform signature for various process invocations;
 
wenzelm 
parents: 
62291 
diff
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: 
61291 
diff
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: 
62291 
diff
changeset
 | 
61  | 
exec(cygwin_root + "\\bin\\dash.exe", "/isabelle/rebaseall")  | 
| 
 
4c89504c76fb
more uniform signature for various process invocations;
 
wenzelm 
parents: 
62291 
diff
changeset
 | 
62  | 
exec(cygwin_root + "\\bin\\bash.exe", "/isabelle/postinstall")  | 
| 61282 | 63  | 
}  | 
64  | 
}  | 
|
65  | 
}  |