87 new BufferedReader(new InputStreamReader(proc.getErrorStream, UTF8.charset)) |
87 new BufferedReader(new InputStreamReader(proc.getErrorStream, UTF8.charset)) |
88 |
88 |
89 |
89 |
90 // signals |
90 // signals |
91 |
91 |
92 private val pid = stdout.readLine |
92 private val group_pid = stdout.readLine |
93 |
93 |
94 @tailrec private def kill(signal: String, count: Int = 1): Boolean = |
94 @tailrec private def signal(s: String, count: Int = 1): Boolean = |
95 { |
95 { |
96 count <= 0 || |
96 count <= 0 || |
97 { |
97 { |
98 Isabelle_System.kill(signal, pid) |
98 Isabelle_System.process_signal(group_pid, signal = s) |
99 val running = Isabelle_System.kill("0", pid)._2 == 0 |
99 val running = Isabelle_System.process_signal(group_pid) |
100 if (running) { |
100 if (running) { |
101 Time.seconds(0.1).sleep |
101 Time.seconds(0.1).sleep |
102 kill(signal, count - 1) |
102 signal(s, count - 1) |
103 } |
103 } |
104 else false |
104 else false |
105 } |
105 } |
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 signal("INT", count = 7) && signal("TERM", count = 3) && signal("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 { |
117 Isabelle_System.kill("INT", pid) |
117 Isabelle_System.process_signal(group_pid, "INT") |
118 } |
118 } |
119 |
119 |
120 |
120 |
121 // JVM shutdown hook |
121 // JVM shutdown hook |
122 |
122 |