equal
deleted
inserted
replaced
9 |
9 |
10 import java.io.{File => JFile, BufferedReader, InputStreamReader, |
10 import java.io.{File => JFile, BufferedReader, InputStreamReader, |
11 BufferedWriter, OutputStreamWriter} |
11 BufferedWriter, OutputStreamWriter} |
12 |
12 |
13 import scala.annotation.tailrec |
13 import scala.annotation.tailrec |
|
14 import scala.jdk.OptionConverters._ |
14 |
15 |
15 |
16 |
16 object Bash |
17 object Bash |
17 { |
18 { |
18 /* concrete syntax */ |
19 /* concrete syntax */ |
89 |
90 |
90 // signals |
91 // signals |
91 |
92 |
92 private val group_pid = stdout.readLine |
93 private val group_pid = stdout.readLine |
93 |
94 |
|
95 private val initial_process: Option[ProcessHandle] = |
|
96 if (Platform.is_unix) ProcessHandle.of(Value.Long.parse(group_pid)).toScala |
|
97 else None |
|
98 |
94 @tailrec private def signal(s: String, count: Int = 1): Boolean = |
99 @tailrec private def signal(s: String, count: Int = 1): Boolean = |
95 { |
100 { |
96 count <= 0 || |
101 count <= 0 || |
97 { |
102 { |
98 Isabelle_System.process_signal(group_pid, signal = s) |
103 Isabelle_System.process_signal(group_pid, signal = s) |
99 val running = Isabelle_System.process_signal(group_pid) |
104 val running = |
|
105 (initial_process.isDefined && initial_process.get.isAlive) || |
|
106 Isabelle_System.process_signal(group_pid) |
100 if (running) { |
107 if (running) { |
101 Time.seconds(0.1).sleep |
108 Time.seconds(0.1).sleep |
102 signal(s, count - 1) |
109 signal(s, count - 1) |
103 } |
110 } |
104 else false |
111 else false |