equal
deleted
inserted
replaced
13 |
13 |
14 |
14 |
15 /* static system */ |
15 /* static system */ |
16 |
16 |
17 def bash(script: String, redirect: Boolean = false, echo: Boolean = false): Process_Result = |
17 def bash(script: String, redirect: Boolean = false, echo: Boolean = false): Process_Result = |
18 Isabelle_System.bash( |
18 progress.bash( |
19 "export ISABELLE_IDENTIFIER=" + File.bash_string(isabelle_identifier) + "\n" + script, |
19 "export ISABELLE_IDENTIFIER=" + File.bash_string(isabelle_identifier) + "\n" + script, |
20 env = null, cwd = isabelle_home.file, redirect = redirect, |
20 env = null, cwd = isabelle_home.file, redirect = redirect) |
21 progress_stdout = progress.echo_if(echo, _), |
|
22 progress_stderr = progress.echo_if(echo, _)) |
|
23 |
21 |
24 def apply(cmdline: String, redirect: Boolean = false, echo: Boolean = false): Process_Result = |
22 def apply(cmdline: String, redirect: Boolean = false, echo: Boolean = false): Process_Result = |
25 bash("bin/isabelle " + cmdline, redirect, echo) |
23 bash("bin/isabelle " + cmdline, redirect, echo) |
26 |
24 |
27 def resolve_components(echo: Boolean): Unit = |
25 def resolve_components(echo: Boolean): Unit = |