src/Pure/System/isabelle_process.scala
changeset 39585 00be8711082f
parent 39575 c77b9374f45c
child 39587 f84b70e3bb9c
     1.1 --- a/src/Pure/System/isabelle_process.scala	Wed Sep 22 12:52:35 2010 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.scala	Wed Sep 22 13:47:48 2010 +0200
     1.3 @@ -92,14 +92,7 @@
     1.4  
     1.5    private def put_result(kind: String, props: List[(String, String)], body: XML.Body)
     1.6    {
     1.7 -    if (pid.isEmpty && kind == Markup.INIT) {
     1.8 -      rm_fifos()
     1.9 -      props.find(_._1 == Markup.PID).map(_._1) match {
    1.10 -        case None => system_result("Bad Isabelle process initialization: missing pid")
    1.11 -        case p => pid = p
    1.12 -      }
    1.13 -    }
    1.14 -
    1.15 +    if (kind == Markup.INIT) rm_fifos()
    1.16      val msg = XML.Elem(Markup(kind, props), Isar_Document.clean_message(body))
    1.17      xml_cache.cache_tree(msg)((message: XML.Tree) =>
    1.18        receiver ! new Result(message.asInstanceOf[XML.Elem]))
    1.19 @@ -117,33 +110,39 @@
    1.20    private case class Input_Chunks(chunks: List[Array[Byte]])
    1.21  
    1.22    private case object Close
    1.23 -  private def close(a: Actor) { if (a != null) a ! Close }
    1.24 +  private def close(p: (Thread, Actor))
    1.25 +  {
    1.26 +    if (p != null && p._1.isAlive) {
    1.27 +      p._2 ! Close
    1.28 +      p._1.join
    1.29 +    }
    1.30 +  }
    1.31  
    1.32 -  @volatile private var standard_input: Actor = null
    1.33 -  @volatile private var command_input: Actor = null
    1.34 +  @volatile private var standard_input: (Thread, Actor) = null
    1.35 +  @volatile private var command_input: (Thread, Actor) = null
    1.36  
    1.37  
    1.38 -  /* process manager */
    1.39 +  /** process manager **/
    1.40  
    1.41    private val in_fifo = system.mk_fifo()
    1.42    private val out_fifo = system.mk_fifo()
    1.43    private def rm_fifos() { system.rm_fifo(in_fifo); system.rm_fifo(out_fifo) }
    1.44  
    1.45 -  private val proc =
    1.46 +  private val process =
    1.47      try {
    1.48        val cmdline =
    1.49          List(system.getenv_strict("ISABELLE_PROCESS"), "-W", in_fifo + ":" + out_fifo) ++ args
    1.50 -      system.execute(true, cmdline: _*)
    1.51 +      new system.Managed_Process(true, cmdline: _*)
    1.52      }
    1.53      catch { case e: IOException => rm_fifos(); throw(e) }
    1.54  
    1.55 -  private val stdout_reader =
    1.56 -    new BufferedReader(new InputStreamReader(proc.getInputStream, Standard_System.charset))
    1.57 +  private def terminate_process()
    1.58 +  {
    1.59 +    try { process.terminate }
    1.60 +    catch { case e: IOException => system_result("Failed to terminate Isabelle: " + e.getMessage) }
    1.61 +  }
    1.62  
    1.63 -  private val stdin_writer =
    1.64 -    new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, Standard_System.charset))
    1.65 -
    1.66 -  private val (process_manager, _) = Simple_Thread.actor("process_manager")
    1.67 +  private val process_manager = Simple_Thread.fork("process_manager")
    1.68    {
    1.69      val (startup_failed, startup_output) =
    1.70      {
    1.71 @@ -152,8 +151,8 @@
    1.72  
    1.73        var finished = false
    1.74        while (!finished && System.currentTimeMillis() <= expired) {
    1.75 -        while (!finished && stdout_reader.ready) {
    1.76 -          val c = stdout_reader.read
    1.77 +        while (!finished && process.stdout.ready) {
    1.78 +          val c = process.stdout.read
    1.79            if (c == 2) finished = true
    1.80            else result += c.toChar
    1.81          }
    1.82 @@ -165,62 +164,45 @@
    1.83  
    1.84      if (startup_failed) {
    1.85        put_result(Markup.EXIT, "127")
    1.86 -      stdin_writer.close
    1.87 -      Thread.sleep(300)  // FIXME !?
    1.88 -      proc.destroy  // FIXME unreliable
    1.89 +      process.stdin.close
    1.90 +      Thread.sleep(300)
    1.91 +      terminate_process()
    1.92      }
    1.93      else {
    1.94        // rendezvous
    1.95        val command_stream = system.fifo_output_stream(in_fifo)
    1.96        val message_stream = system.fifo_input_stream(out_fifo)
    1.97  
    1.98 -      val stdin = stdin_actor(); standard_input = stdin._2
    1.99 +      standard_input = stdin_actor()
   1.100        val stdout = stdout_actor()
   1.101 -      val input = input_actor(command_stream); command_input = input._2
   1.102 +      command_input = input_actor(command_stream)
   1.103        val message = message_actor(message_stream)
   1.104  
   1.105 -      val rc = proc.waitFor()
   1.106 +      val rc = process.join
   1.107        system_result("Isabelle process terminated")
   1.108 -      for ((thread, _) <- List(stdin, stdout, input, message)) thread.join
   1.109 +      for ((thread, _) <- List(standard_input, stdout, command_input, message)) thread.join
   1.110        system_result("process_manager terminated")
   1.111        put_result(Markup.EXIT, rc.toString)
   1.112      }
   1.113      rm_fifos()
   1.114    }
   1.115  
   1.116 -  def join() { process_manager.join() }
   1.117 -
   1.118  
   1.119 -  /* signals */
   1.120 +  /* management methods */
   1.121  
   1.122 -  @volatile private var pid: Option[String] = None
   1.123 +  def join() { process_manager.join() }
   1.124  
   1.125    def interrupt()
   1.126    {
   1.127 -    pid match {
   1.128 -      case None => system_result("Cannot interrupt Isabelle: unknown pid")
   1.129 -      case Some(i) =>
   1.130 -        try {
   1.131 -          if (system.execute(true, "kill", "-INT", i).waitFor == 0)
   1.132 -            system_result("Interrupt Isabelle")
   1.133 -          else
   1.134 -            system_result("Cannot interrupt Isabelle: kill command failed")
   1.135 -        }
   1.136 -        catch { case e: IOException => error("Cannot interrupt Isabelle: " + e.getMessage) }
   1.137 -    }
   1.138 +    try { process.interrupt }
   1.139 +    catch { case e: IOException => system_result("Failed to interrupt Isabelle: " + e.getMessage) }
   1.140    }
   1.141  
   1.142 -  def kill()
   1.143 +  def terminate()
   1.144    {
   1.145 -    val running =
   1.146 -      try { proc.exitValue; false }
   1.147 -      catch { case e: java.lang.IllegalThreadStateException => true }
   1.148 -    if (running) {
   1.149 -      close()
   1.150 -      Thread.sleep(500)  // FIXME !?
   1.151 -      system_result("Kill Isabelle")
   1.152 -      proc.destroy
   1.153 -    }
   1.154 +    close()
   1.155 +    system_result("Terminating Isabelle process")
   1.156 +    terminate_process()
   1.157    }
   1.158  
   1.159  
   1.160 @@ -239,10 +221,10 @@
   1.161            //{{{
   1.162            receive {
   1.163              case Input_Text(text) =>
   1.164 -              stdin_writer.write(text)
   1.165 -              stdin_writer.flush
   1.166 +              process.stdin.write(text)
   1.167 +              process.stdin.flush
   1.168              case Close =>
   1.169 -              stdin_writer.close
   1.170 +              process.stdin.close
   1.171                finished = true
   1.172              case bad => System.err.println(name + ": ignoring bad message " + bad)
   1.173            }
   1.174 @@ -269,8 +251,8 @@
   1.175            //{{{
   1.176            var c = -1
   1.177            var done = false
   1.178 -          while (!done && (result.length == 0 || stdout_reader.ready)) {
   1.179 -            c = stdout_reader.read
   1.180 +          while (!done && (result.length == 0 || process.stdout.ready)) {
   1.181 +            c = process.stdout.read
   1.182              if (c >= 0) result.append(c.asInstanceOf[Char])
   1.183              else done = true
   1.184            }
   1.185 @@ -279,7 +261,7 @@
   1.186              result.length = 0
   1.187            }
   1.188            else {
   1.189 -            stdout_reader.close
   1.190 +            process.stdout.close
   1.191              finished = true
   1.192            }
   1.193            //}}}
   1.194 @@ -391,10 +373,10 @@
   1.195  
   1.196    /** main methods **/
   1.197  
   1.198 -  def input_raw(text: String): Unit = standard_input ! Input_Text(text)
   1.199 +  def input_raw(text: String): Unit = standard_input._2 ! Input_Text(text)
   1.200  
   1.201    def input_bytes(name: String, args: Array[Byte]*): Unit =
   1.202 -    command_input ! Input_Chunks(Standard_System.string_bytes(name) :: args.toList)
   1.203 +    command_input._2 ! Input_Chunks(Standard_System.string_bytes(name) :: args.toList)
   1.204  
   1.205    def input(name: String, args: String*): Unit =
   1.206      input_bytes(name, args.map(Standard_System.string_bytes): _*)