41 override def toString: String = isabelle_home_url |
41 override def toString: String = isabelle_home_url |
42 |
42 |
43 |
43 |
44 /* static system */ |
44 /* static system */ |
45 |
45 |
|
46 def bash_context(script: String): String = |
|
47 Bash.context(script, |
|
48 user_home = ssh.user_home, |
|
49 isabelle_identifier = isabelle_identifier, |
|
50 cwd = isabelle_home) |
|
51 |
46 def bash( |
52 def bash( |
47 script: String, |
53 script: String, |
48 redirect: Boolean = false, |
54 redirect: Boolean = false, |
49 echo: Boolean = false, |
55 echo: Boolean = false, |
50 strict: Boolean = true |
56 strict: Boolean = true |
51 ): Process_Result = { |
57 ): Process_Result = { |
52 val env = |
58 ssh.execute(bash_context(script), |
53 Isabelle_System.export_env( |
|
54 user_home = ssh.user_home, |
|
55 isabelle_identifier = isabelle_identifier) |
|
56 ssh.execute(env + "cd " + ssh.bash_path(isabelle_home) + "\n" + script, |
|
57 progress_stdout = progress.echo_if(echo, _), |
59 progress_stdout = progress.echo_if(echo, _), |
58 progress_stderr = progress.echo_if(echo, _), |
60 progress_stderr = progress.echo_if(echo, _), |
59 redirect = redirect, |
61 redirect = redirect, |
60 settings = false, |
62 settings = false, |
61 strict = strict) |
63 strict = strict) |