59 |
59 |
60 def cygwin_init(isabelle_root: String, cygwin_root: String): Unit = |
60 def cygwin_init(isabelle_root: String, cygwin_root: String): Unit = |
61 { |
61 { |
62 require(Platform.is_windows, "Windows platform expected") |
62 require(Platform.is_windows, "Windows platform expected") |
63 |
63 |
64 def exec(cmdline: JList[String]): Unit = |
64 def cygwin_exec(cmd: JList[String]): Unit = |
65 { |
65 { |
66 val cwd = new JFile(isabelle_root) |
66 val cwd = new JFile(isabelle_root) |
67 val env = sys.env + ("CYGWIN" -> "nodosfilewarning") |
67 val env = sys.env + ("CYGWIN" -> "nodosfilewarning") |
68 val (output, rc) = |
68 val res = exec_process(cmd, cwd = cwd, env = env, redirect = true) |
69 Isabelle_Env.process_output(Isabelle_Env.process(cmdline, cwd = cwd, env = env, redirect = true)) |
69 if (!res.ok) error(res.out) |
70 if (rc != 0) error(output) |
|
71 } |
70 } |
72 |
71 |
73 val uninitialized_file = new JFile(cygwin_root, "isabelle\\uninitialized") |
72 val uninitialized_file = new JFile(cygwin_root, "isabelle\\uninitialized") |
74 val uninitialized = uninitialized_file.isFile && uninitialized_file.delete |
73 val uninitialized = uninitialized_file.isFile && uninitialized_file.delete |
75 |
74 |
89 case _ => error("Unbalanced symlinks list") |
88 case _ => error("Unbalanced symlinks list") |
90 } |
89 } |
91 } |
90 } |
92 recover_symlinks(symlinks) |
91 recover_symlinks(symlinks) |
93 |
92 |
94 exec(JList.of(cygwin_root + "\\bin\\dash.exe", "/isabelle/rebaseall")) |
93 cygwin_exec(JList.of(cygwin_root + "\\bin\\dash.exe", "/isabelle/rebaseall")) |
95 exec(JList.of(cygwin_root + "\\bin\\bash.exe", "/isabelle/postinstall")) |
94 cygwin_exec(JList.of(cygwin_root + "\\bin\\bash.exe", "/isabelle/postinstall")) |
96 } |
95 } |
97 } |
96 } |
98 |
97 |
99 |
98 |
100 |
99 |
101 /** raw process **/ |
100 /** raw process **/ |
102 |
101 |
103 /* raw process */ |
102 /* raw process */ |
104 |
103 |
105 def process(command_line: JList[String], |
104 def process_builder(cmd: JList[String], |
106 cwd: JFile = null, |
105 cwd: JFile = null, |
107 env: Map[String, String] = settings(), |
106 env: Map[String, String] = settings(), |
108 redirect: Boolean = false): Process = |
107 redirect: Boolean = false): ProcessBuilder = |
109 { |
108 { |
110 val proc = new ProcessBuilder |
109 val builder = new ProcessBuilder |
111 |
110 |
112 // fragile on Windows: |
111 // fragile on Windows: |
113 // see https://docs.microsoft.com/en-us/cpp/cpp/main-function-command-line-args?view=msvc-160 |
112 // see https://docs.microsoft.com/en-us/cpp/cpp/main-function-command-line-args?view=msvc-160 |
114 proc.command(command_line) |
113 builder.command(cmd) |
115 |
114 |
116 if (cwd != null) proc.directory(cwd) |
115 if (cwd != null) builder.directory(cwd) |
117 if (env != null) { |
116 if (env != null) { |
118 proc.environment.clear() |
117 builder.environment.clear() |
119 for ((x, y) <- env) proc.environment.put(x, y) |
118 for ((x, y) <- env) builder.environment.put(x, y) |
120 } |
119 } |
121 proc.redirectErrorStream(redirect) |
120 builder.redirectErrorStream(redirect) |
122 proc.start |
121 } |
123 } |
122 |
124 |
123 class Exec_Result(val rc: Int, val out: String, val err: String) |
125 def process_output(proc: Process): (String, Int) = |
124 { |
126 { |
125 def ok: Boolean = rc == 0 |
127 proc.getOutputStream.close() |
126 } |
128 |
127 |
129 val output = File.read_stream(proc.getInputStream) |
128 def exec_process(command_line: JList[String], |
130 val rc = |
129 cwd: JFile = null, |
131 try { proc.waitFor } |
130 env: Map[String, String] = settings(), |
|
131 redirect: Boolean = false): Exec_Result = |
|
132 { |
|
133 val out_file = Files.createTempFile(null, null) |
|
134 val err_file = Files.createTempFile(null, null) |
|
135 try { |
|
136 val proc = |
|
137 { |
|
138 val builder = process_builder(command_line, cwd = cwd, env = env, redirect = redirect) |
|
139 builder.redirectOutput(out_file.toFile) |
|
140 builder.redirectError(err_file.toFile) |
|
141 builder.start() |
|
142 } |
|
143 proc.getOutputStream.close() |
|
144 try { proc.waitFor() } |
132 finally { |
145 finally { |
133 proc.getInputStream.close() |
146 proc.getInputStream.close() |
134 proc.getErrorStream.close() |
147 proc.getErrorStream.close() |
135 proc.destroy() |
148 proc.destroy() |
136 Exn.Interrupt.dispose() |
149 Thread.interrupted() |
137 } |
150 } |
138 (output, rc) |
151 |
|
152 val rc = proc.exitValue() |
|
153 val out = Files.readString(out_file) |
|
154 val err = Files.readString(err_file) |
|
155 new Exec_Result(rc, out, err) |
|
156 } |
|
157 finally { |
|
158 Files.deleteIfExists(out_file) |
|
159 Files.deleteIfExists(err_file) |
|
160 } |
139 } |
161 } |
140 |
162 |
141 |
163 |
142 |
164 |
143 /** implicit settings environment **/ |
165 /** implicit settings environment **/ |
208 } |
230 } |
209 cmd.add("getenv") |
231 cmd.add("getenv") |
210 cmd.add("-d") |
232 cmd.add("-d") |
211 cmd.add(dump.toString) |
233 cmd.add(dump.toString) |
212 |
234 |
213 val (output, rc) = process_output(process(cmd, env = env, redirect = true)) |
235 val res = exec_process(cmd, env = env, redirect = true) |
214 if (rc != 0) error(output) |
236 if (!res.ok) error(res.out) |
215 |
237 |
216 val entries = |
238 val entries = |
217 space_explode('\u0000', File.read(dump)).flatMap( |
239 space_explode('\u0000', File.read(dump)).flatMap( |
218 { |
240 { |
219 case Properties.Eq(a, b) => Some(a -> b) |
241 case Properties.Eq(a, b) => Some(a -> b) |