71 val shell_prefix = |
71 val shell_prefix = |
72 if (Platform.is_windows) List(standard_system.platform_root + "\\bin\\bash", "-l") |
72 if (Platform.is_windows) List(standard_system.platform_root + "\\bin\\bash", "-l") |
73 else Nil |
73 else Nil |
74 val cmdline = |
74 val cmdline = |
75 shell_prefix ::: List(isabelle_home + "/bin/isabelle", "getenv", "-d", dump.toString) |
75 shell_prefix ::: List(isabelle_home + "/bin/isabelle", "getenv", "-d", dump.toString) |
76 val (output, rc) = Standard_System.raw_exec(null, env, true, cmdline: _*) |
76 val (output, rc) = process_output(raw_execute(null, env, true, cmdline: _*)) |
77 if (rc != 0) error(output) |
77 if (rc != 0) error(output) |
78 |
78 |
79 val entries = |
79 val entries = |
80 (for (entry <- File.read(dump) split "\0" if entry != "") yield { |
80 (for (entry <- File.read(dump) split "\0" if entry != "") yield { |
81 val i = entry.indexOf('=') |
81 val i = entry.indexOf('=') |
138 |
138 |
139 |
139 |
140 |
140 |
141 /** external processes **/ |
141 /** external processes **/ |
142 |
142 |
|
143 /* raw execute for bootstrapping */ |
|
144 |
|
145 private def raw_execute(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*) |
|
146 : Process = |
|
147 { |
|
148 val cmdline = new java.util.LinkedList[String] |
|
149 for (s <- args) cmdline.add(s) |
|
150 |
|
151 val proc = new ProcessBuilder(cmdline) |
|
152 if (cwd != null) proc.directory(cwd) |
|
153 if (env != null) { |
|
154 proc.environment.clear |
|
155 for ((x, y) <- env) proc.environment.put(x, y) |
|
156 } |
|
157 proc.redirectErrorStream(redirect) |
|
158 proc.start |
|
159 } |
|
160 |
|
161 private def process_output(proc: Process): (String, Int) = |
|
162 { |
|
163 proc.getOutputStream.close |
|
164 val output = File.read(proc.getInputStream) |
|
165 val rc = |
|
166 try { proc.waitFor } |
|
167 finally { |
|
168 proc.getInputStream.close |
|
169 proc.getErrorStream.close |
|
170 proc.destroy |
|
171 Thread.interrupted |
|
172 } |
|
173 (output, rc) |
|
174 } |
|
175 |
|
176 |
143 /* plain execute */ |
177 /* plain execute */ |
144 |
178 |
145 def execute_env(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process = |
179 def execute_env(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process = |
146 { |
180 { |
147 val cmdline = |
181 val cmdline = |
148 if (Platform.is_windows) List(standard_system.platform_root + "\\bin\\env.exe") ++ args |
182 if (Platform.is_windows) List(standard_system.platform_root + "\\bin\\env.exe") ++ args |
149 else args |
183 else args |
150 val env1 = if (env == null) settings else settings ++ env |
184 val env1 = if (env == null) settings else settings ++ env |
151 Standard_System.raw_execute(cwd, env1, redirect, cmdline: _*) |
185 raw_execute(cwd, env1, redirect, cmdline: _*) |
152 } |
186 } |
153 |
187 |
154 def execute(redirect: Boolean, args: String*): Process = |
188 def execute(redirect: Boolean, args: String*): Process = |
155 execute_env(null, null, redirect, args: _*) |
189 execute_env(null, null, redirect, args: _*) |
156 |
190 |
256 } |
290 } |
257 catch { case _: SecurityException => false } |
291 catch { case _: SecurityException => false } |
258 } match { |
292 } match { |
259 case Some(dir) => |
293 case Some(dir) => |
260 val file = standard_path(dir + Path.basic(name)) |
294 val file = standard_path(dir + Path.basic(name)) |
261 Standard_System.process_output(execute(true, (List(file) ++ args): _*)) |
295 process_output(execute(true, (List(file) ++ args): _*)) |
262 case None => ("Unknown Isabelle tool: " + name, 2) |
296 case None => ("Unknown Isabelle tool: " + name, 2) |
263 } |
297 } |
264 } |
298 } |
265 |
299 |
266 |
300 |