changeset 62569 | 5db10482f4cf |
parent 62558 | c46418f12ee1 |
child 62573 | 27f90319a499 |
62568:3541bc1e97d2 | 62569:5db10482f4cf |
---|---|
32 |
32 |
33 class Process private [Bash]( |
33 class Process private [Bash]( |
34 script: String, cwd: JFile, env: Map[String, String], redirect: Boolean) |
34 script: String, cwd: JFile, env: Map[String, String], redirect: Boolean) |
35 extends Prover.System_Process |
35 extends Prover.System_Process |
36 { |
36 { |
37 val script_file = Isabelle_System.tmp_file("bash_script") |
37 private val timing_file = Isabelle_System.tmp_file("bash_script") |
38 private val timing = Synchronized[Option[Timing]](None) |
|
39 |
|
40 private val script_file = Isabelle_System.tmp_file("bash_script") |
|
38 File.write(script_file, script) |
41 File.write(script_file, script) |
39 |
42 |
40 private val proc = |
43 private val proc = |
41 Isabelle_System.process(cwd, Isabelle_System.settings(env), redirect, |
44 Isabelle_System.process(cwd, Isabelle_System.settings(env), redirect, |
42 File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")), "-", |
45 File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")), "-", |
43 "bash", File.standard_path(script_file)) |
46 File.standard_path(timing_file), "bash", File.standard_path(script_file)) |
44 |
47 |
45 |
48 |
46 // channels |
49 // channels |
47 |
50 |
48 val stdin: BufferedWriter = |
51 val stdin: BufferedWriter = |
103 try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) } |
106 try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) } |
104 catch { case _: IllegalStateException => } |
107 catch { case _: IllegalStateException => } |
105 |
108 |
106 script_file.delete |
109 script_file.delete |
107 |
110 |
111 timing.change { |
|
112 case None => |
|
113 val t = |
|
114 Word.explode(File.read(timing_file)) match { |
|
115 case List(Properties.Value.Long(elapsed), Properties.Value.Long(cpu)) => |
|
116 Timing(Time.ms(elapsed), Time.ms(cpu), Time.zero) |
|
117 case _ => Timing.zero |
|
118 } |
|
119 timing_file.delete |
|
120 Some(t) |
|
121 case some => some |
|
122 } |
|
123 |
|
108 rc |
124 rc |
109 } |
125 } |
110 |
126 |
111 |
127 |
112 /* result */ |
128 /* result */ |
128 val rc = |
144 val rc = |
129 try { join } |
145 try { join } |
130 catch { case Exn.Interrupt() => terminate; Exn.Interrupt.return_code } |
146 catch { case Exn.Interrupt() => terminate; Exn.Interrupt.return_code } |
131 if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt() |
147 if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt() |
132 |
148 |
133 Process_Result(rc, out_lines.join, err_lines.join) |
149 Process_Result(rc, out_lines.join, err_lines.join, false, timing.value.get) |
134 } |
150 } |
135 } |
151 } |
136 } |
152 } |