src/Pure/System/bash.scala
changeset 73858 37243ad3ecb6
parent 73857 19c558ea903c
child 73859 342362c9496c
equal deleted inserted replaced
73857:19c558ea903c 73858:37243ad3ecb6
     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