equal
deleted
inserted
replaced
26 } |
26 } |
27 } |
27 } |
28 |
28 |
29 def process(script: String, |
29 def process(script: String, |
30 cwd: JFile = null, |
30 cwd: JFile = null, |
31 env: Map[String, String] = Map.empty, |
31 env: Map[String, String] = Isabelle_System.settings(), |
32 redirect: Boolean = false, |
32 redirect: Boolean = false, |
33 cleanup: () => Unit = () => ()): Process = |
33 cleanup: () => Unit = () => ()): Process = |
34 new Process(script, cwd, env, redirect, cleanup) |
34 new Process(script, cwd, env, redirect, cleanup) |
35 |
35 |
36 class Process private [Bash]( |
36 class Process private [Bash]( |
46 |
46 |
47 private val script_file = Isabelle_System.tmp_file("bash_script") |
47 private val script_file = Isabelle_System.tmp_file("bash_script") |
48 File.write(script_file, script) |
48 File.write(script_file, script) |
49 |
49 |
50 private val proc = |
50 private val proc = |
51 Isabelle_System.process(cwd, Isabelle_System.settings(env), redirect, |
51 Isabelle_System.process( |
52 File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")), "-", |
52 List(File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")), "-", |
53 File.standard_path(timing_file), "bash", File.standard_path(script_file)) |
53 File.standard_path(timing_file), "bash", File.standard_path(script_file)), |
|
54 cwd = cwd, env = env, redirect = redirect) |
54 |
55 |
55 |
56 |
56 // channels |
57 // channels |
57 |
58 |
58 val stdin: BufferedWriter = |
59 val stdin: BufferedWriter = |