equal
deleted
inserted
replaced
98 |
98 |
99 // signals |
99 // signals |
100 |
100 |
101 private val pid = stdout.readLine |
101 private val pid = stdout.readLine |
102 |
102 |
103 def interrupt() |
|
104 { Exn.Interrupt.postpone { Isabelle_System.kill("INT", pid) } } |
|
105 |
|
106 private def kill(signal: String): Boolean = |
103 private def kill(signal: String): Boolean = |
107 Exn.Interrupt.postpone { |
104 { |
108 Isabelle_System.kill(signal, pid) |
105 Isabelle_System.kill(signal, pid) |
109 Isabelle_System.kill("0", pid)._2 == 0 } getOrElse true |
106 Isabelle_System.kill("0", pid)._2 == 0 |
|
107 } |
110 |
108 |
111 private def multi_kill(signal: String): Boolean = |
109 private def multi_kill(signal: String): Boolean = |
112 { |
110 { |
113 var running = true |
111 var running = true |
114 var count = 10 |
112 var count = 10 |
115 while (running && count > 0) { |
113 while (running && count > 0) { |
116 if (kill(signal)) { |
114 if (kill(signal)) { |
117 Exn.Interrupt.postpone { |
115 Time.seconds(0.1).sleep |
118 Time.seconds(0.1).sleep |
116 count -= 1 |
119 count -= 1 |
|
120 } |
|
121 } |
117 } |
122 else running = false |
118 else running = false |
123 } |
119 } |
124 running |
120 running |
125 } |
121 } |
126 |
122 |
127 def terminate() |
123 def terminate(): Unit = Isabelle_Thread.uninterruptible |
128 { |
124 { |
129 multi_kill("INT") && multi_kill("TERM") && kill("KILL") |
125 multi_kill("INT") && multi_kill("TERM") && kill("KILL") |
130 proc.destroy |
126 proc.destroy |
131 do_cleanup() |
127 do_cleanup() |
|
128 } |
|
129 |
|
130 def interrupt(): Unit = Isabelle_Thread.uninterruptible |
|
131 { |
|
132 Isabelle_System.kill("INT", pid) |
132 } |
133 } |
133 |
134 |
134 |
135 |
135 // JVM shutdown hook |
136 // JVM shutdown hook |
136 |
137 |