equal
deleted
inserted
replaced
106 } |
106 } |
107 |
107 |
108 def terminate(): Unit = Isabelle_Thread.try_uninterruptible |
108 def terminate(): Unit = Isabelle_Thread.try_uninterruptible |
109 { |
109 { |
110 kill("INT", count = 7) && kill("TERM", count = 3) && kill("KILL") |
110 kill("INT", count = 7) && kill("TERM", count = 3) && kill("KILL") |
111 proc.destroy |
111 proc.destroy() |
112 do_cleanup() |
112 do_cleanup() |
113 } |
113 } |
114 |
114 |
115 def interrupt(): Unit = Isabelle_Thread.try_uninterruptible |
115 def interrupt(): Unit = Isabelle_Thread.try_uninterruptible |
116 { |
116 { |
171 progress_stdout: String => Unit = (_: String) => (), |
171 progress_stdout: String => Unit = (_: String) => (), |
172 progress_stderr: String => Unit = (_: String) => (), |
172 progress_stderr: String => Unit = (_: String) => (), |
173 watchdog: Option[Watchdog] = None, |
173 watchdog: Option[Watchdog] = None, |
174 strict: Boolean = true): Process_Result = |
174 strict: Boolean = true): Process_Result = |
175 { |
175 { |
176 stdin.close |
176 stdin.close() |
177 |
177 |
178 val out_lines = |
178 val out_lines = |
179 Future.thread("bash_stdout") { File.read_lines(stdout, progress_stdout) } |
179 Future.thread("bash_stdout") { File.read_lines(stdout, progress_stdout) } |
180 val err_lines = |
180 val err_lines = |
181 Future.thread("bash_stderr") { File.read_lines(stderr, progress_stderr) } |
181 Future.thread("bash_stderr") { File.read_lines(stderr, progress_stderr) } |
193 |
193 |
194 val rc = |
194 val rc = |
195 try { join } |
195 try { join } |
196 catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code } |
196 catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code } |
197 |
197 |
198 watchdog_thread.foreach(_.cancel) |
198 watchdog_thread.foreach(_.cancel()) |
199 |
199 |
200 if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt() |
200 if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt() |
201 |
201 |
202 Process_Result(rc, out_lines.join, err_lines.join, get_timing) |
202 Process_Result(rc, out_lines.join, err_lines.join, get_timing) |
203 } |
203 } |