1.1 --- a/src/Pure/General/markup.ML	Wed Sep 22 12:52:35 2010 +0200
     1.2 +++ b/src/Pure/General/markup.ML	Wed Sep 22 13:47:48 2010 +0200
     1.3 @@ -114,7 +114,6 @@
     1.4    val execN: string
     1.5    val assignN: string val assign: int -> T
     1.6    val editN: string val edit: int -> int -> T
     1.7 -  val pidN: string
     1.8    val serialN: string
     1.9    val promptN: string val prompt: T
    1.10    val readyN: string val ready: T
    1.11 @@ -340,7 +339,6 @@
    1.12  
    1.13  (* messages *)
    1.14  
    1.15 -val pidN = "pid";
    1.16  val serialN = "serial";
    1.17  
    1.18  val (promptN, prompt) = markup_elem "prompt";

     2.1 --- a/src/Pure/General/markup.scala	Wed Sep 22 12:52:35 2010 +0200
     2.2 +++ b/src/Pure/General/markup.scala	Wed Sep 22 13:47:48 2010 +0200
     2.3 @@ -227,7 +227,6 @@
     2.4  
     2.5    /* messages */
     2.6  
     2.7 -  val PID = "pid"
     2.8    val Serial = new Long_Property("serial")
     2.9  
    2.10    val MESSAGE = "message"

     3.1 --- a/src/Pure/ML-Systems/polyml_common.ML	Wed Sep 22 12:52:35 2010 +0200
     3.2 +++ b/src/Pure/ML-Systems/polyml_common.ML	Wed Sep 22 13:47:48 2010 +0200
     3.3 @@ -111,9 +111,6 @@
     3.4  val cd = OS.FileSys.chDir;
     3.5  val pwd = OS.FileSys.getDir;
     3.6  
     3.7 -fun process_id () =
     3.8 -  Word.fmt StringCvt.DEC (Word.fromLargeWord (Posix.Process.pidToWord (Posix.ProcEnv.getpid ())));
     3.9 -
    3.10  
    3.11  (* getenv *)
    3.12  

     4.1 --- a/src/Pure/ML-Systems/smlnj.ML	Wed Sep 22 12:52:35 2010 +0200
     4.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Wed Sep 22 13:47:48 2010 +0200
     4.3 @@ -172,9 +172,6 @@
     4.4  
     4.5  val bash_output = (fn (output, rc) => (output, mk_int rc)) o bash_output;
     4.6  
     4.7 -fun process_id pid =
     4.8 -  Word.fmt StringCvt.DEC (Word.fromLargeWord (Posix.Process.pidToWord (Posix.ProcEnv.getpid ())));
     4.9 -
    4.10  
    4.11  (* getenv *)
    4.12  

     5.1 --- a/src/Pure/System/isabelle_process.ML	Wed Sep 22 12:52:35 2010 +0200
     5.2 +++ b/src/Pure/System/isabelle_process.ML	Wed Sep 22 13:47:48 2010 +0200
     5.3 @@ -78,7 +78,7 @@
     5.4        (Position.properties_of (Position.thread_data ()))) body;
     5.5  
     5.6  fun init_message out_stream =
     5.7 -  message out_stream "A" [(Markup.pidN, process_id ())] (Session.welcome ());
     5.8 +  message out_stream "A" [] (Session.welcome ());
     5.9  
    5.10  end;
    5.11  

     6.1 --- a/src/Pure/System/isabelle_process.scala	Wed Sep 22 12:52:35 2010 +0200
     6.2 +++ b/src/Pure/System/isabelle_process.scala	Wed Sep 22 13:47:48 2010 +0200
     6.3 @@ -92,14 +92,7 @@
     6.4  
     6.5    private def put_result(kind: String, props: List[(String, String)], body: XML.Body)
     6.6    {
     6.7 -    if (pid.isEmpty && kind == Markup.INIT) {
     6.8 -      rm_fifos()
     6.9 -      props.find(_._1 == Markup.PID).map(_._1) match {
    6.10 -        case None => system_result("Bad Isabelle process initialization: missing pid")
    6.11 -        case p => pid = p
    6.12 -      }
    6.13 -    }
    6.14 -
    6.15 +    if (kind == Markup.INIT) rm_fifos()
    6.16      val msg = XML.Elem(Markup(kind, props), Isar_Document.clean_message(body))
    6.17      xml_cache.cache_tree(msg)((message: XML.Tree) =>
    6.18        receiver ! new Result(message.asInstanceOf[XML.Elem]))
    6.19 @@ -117,33 +110,39 @@
    6.20    private case class Input_Chunks(chunks: List[Array[Byte]])
    6.21  
    6.22    private case object Close
    6.23 -  private def close(a: Actor) { if (a != null) a ! Close }
    6.24 +  private def close(p: (Thread, Actor))
    6.25 +  {
    6.26 +    if (p != null && p._1.isAlive) {
    6.27 +      p._2 ! Close
    6.28 +      p._1.join
    6.29 +    }
    6.30 +  }
    6.31  
    6.32 -  @volatile private var standard_input: Actor = null
    6.33 -  @volatile private var command_input: Actor = null
    6.34 +  @volatile private var standard_input: (Thread, Actor) = null
    6.35 +  @volatile private var command_input: (Thread, Actor) = null
    6.36  
    6.37  
    6.38 -  /* process manager */
    6.39 +  /** process manager **/
    6.40  
    6.41    private val in_fifo = system.mk_fifo()
    6.42    private val out_fifo = system.mk_fifo()
    6.43    private def rm_fifos() { system.rm_fifo(in_fifo); system.rm_fifo(out_fifo) }
    6.44  
    6.45 -  private val proc =
    6.46 +  private val process =
    6.47      try {
    6.48        val cmdline =
    6.49          List(system.getenv_strict("ISABELLE_PROCESS"), "-W", in_fifo + ":" + out_fifo) ++ args
    6.50 -      system.execute(true, cmdline: _*)
    6.51 +      new system.Managed_Process(true, cmdline: _*)
    6.52      }
    6.53      catch { case e: IOException => rm_fifos(); throw(e) }
    6.54  
    6.55 -  private val stdout_reader =
    6.56 -    new BufferedReader(new InputStreamReader(proc.getInputStream, Standard_System.charset))
    6.57 +  private def terminate_process()
    6.58 +  {
    6.59 +    try { process.terminate }
    6.60 +    catch { case e: IOException => system_result("Failed to terminate Isabelle: " + e.getMessage) }
    6.61 +  }
    6.62  
    6.63 -  private val stdin_writer =
    6.64 -    new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, Standard_System.charset))
    6.65 -
    6.66 -  private val (process_manager, _) = Simple_Thread.actor("process_manager")
    6.67 +  private val process_manager = Simple_Thread.fork("process_manager")
    6.68    {
    6.69      val (startup_failed, startup_output) =
    6.70      {
    6.71 @@ -152,8 +151,8 @@
    6.72  
    6.73        var finished = false
    6.74        while (!finished && System.currentTimeMillis() <= expired) {
    6.75 -        while (!finished && stdout_reader.ready) {
    6.76 -          val c = stdout_reader.read
    6.77 +        while (!finished && process.stdout.ready) {
    6.78 +          val c = process.stdout.read
    6.79            if (c == 2) finished = true
    6.80            else result += c.toChar
    6.81          }
    6.82 @@ -165,62 +164,45 @@
    6.83  
    6.84      if (startup_failed) {
    6.85        put_result(Markup.EXIT, "127")
    6.86 -      stdin_writer.close
    6.87 -      Thread.sleep(300)  // FIXME !?
    6.88 -      proc.destroy  // FIXME unreliable
    6.89 +      process.stdin.close
    6.90 +      Thread.sleep(300)
    6.91 +      terminate_process()
    6.92      }
    6.93      else {
    6.94        // rendezvous
    6.95        val command_stream = system.fifo_output_stream(in_fifo)
    6.96        val message_stream = system.fifo_input_stream(out_fifo)
    6.97  
    6.98 -      val stdin = stdin_actor(); standard_input = stdin._2
    6.99 +      standard_input = stdin_actor()
   6.100        val stdout = stdout_actor()
   6.101 -      val input = input_actor(command_stream); command_input = input._2
   6.102 +      command_input = input_actor(command_stream)
   6.103        val message = message_actor(message_stream)
   6.104  
   6.105 -      val rc = proc.waitFor()
   6.106 +      val rc = process.join
   6.107        system_result("Isabelle process terminated")
   6.108 -      for ((thread, _) <- List(stdin, stdout, input, message)) thread.join
   6.109 +      for ((thread, _) <- List(standard_input, stdout, command_input, message)) thread.join
   6.110        system_result("process_manager terminated")
   6.111        put_result(Markup.EXIT, rc.toString)
   6.112      }
   6.113      rm_fifos()
   6.114    }
   6.115  
   6.116 +
   6.117 +  /* management methods */
   6.118 +
   6.119    def join() { process_manager.join() }
   6.120  
   6.121 -
   6.122 -  /* signals */
   6.123 -
   6.124 -  @volatile private var pid: Option[String] = None
   6.125 -
   6.126    def interrupt()
   6.127    {
   6.128 -    pid match {
   6.129 -      case None => system_result("Cannot interrupt Isabelle: unknown pid")
   6.130 -      case Some(i) =>
   6.131 -        try {
   6.132 -          if (system.execute(true, "kill", "-INT", i).waitFor == 0)
   6.133 -            system_result("Interrupt Isabelle")
   6.134 -          else
   6.135 -            system_result("Cannot interrupt Isabelle: kill command failed")
   6.136 -        }
   6.137 -        catch { case e: IOException => error("Cannot interrupt Isabelle: " + e.getMessage) }
   6.138 -    }
   6.139 +    try { process.interrupt }
   6.140 +    catch { case e: IOException => system_result("Failed to interrupt Isabelle: " + e.getMessage) }
   6.141    }
   6.142  
   6.143 -  def kill()
   6.144 +  def terminate()
   6.145    {
   6.146 -    val running =
   6.147 -      try { proc.exitValue; false }
   6.148 -      catch { case e: java.lang.IllegalThreadStateException => true }
   6.149 -    if (running) {
   6.150 -      close()
   6.151 -      Thread.sleep(500)  // FIXME !?
   6.152 -      system_result("Kill Isabelle")
   6.153 -      proc.destroy
   6.154 -    }
   6.155 +    close()
   6.156 +    system_result("Terminating Isabelle process")
   6.157 +    terminate_process()
   6.158    }
   6.159  
   6.160  
   6.161 @@ -239,10 +221,10 @@
   6.162            //{{{
   6.163            receive {
   6.164              case Input_Text(text) =>
   6.165 -              stdin_writer.write(text)
   6.166 -              stdin_writer.flush
   6.167 +              process.stdin.write(text)
   6.168 +              process.stdin.flush
   6.169              case Close =>
   6.170 -              stdin_writer.close
   6.171 +              process.stdin.close
   6.172                finished = true
   6.173              case bad => System.err.println(name + ": ignoring bad message " + bad)
   6.174            }
   6.175 @@ -269,8 +251,8 @@
   6.176            //{{{
   6.177            var c = -1
   6.178            var done = false
   6.179 -          while (!done && (result.length == 0 || stdout_reader.ready)) {
   6.180 -            c = stdout_reader.read
   6.181 +          while (!done && (result.length == 0 || process.stdout.ready)) {
   6.182 +            c = process.stdout.read
   6.183              if (c >= 0) result.append(c.asInstanceOf[Char])
   6.184              else done = true
   6.185            }
   6.186 @@ -279,7 +261,7 @@
   6.187              result.length = 0
   6.188            }
   6.189            else {
   6.190 -            stdout_reader.close
   6.191 +            process.stdout.close
   6.192              finished = true
   6.193            }
   6.194            //}}}
   6.195 @@ -391,10 +373,10 @@
   6.196  
   6.197    /** main methods **/
   6.198  
   6.199 -  def input_raw(text: String): Unit = standard_input ! Input_Text(text)
   6.200 +  def input_raw(text: String): Unit = standard_input._2 ! Input_Text(text)
   6.201  
   6.202    def input_bytes(name: String, args: Array[Byte]*): Unit =
   6.203 -    command_input ! Input_Chunks(Standard_System.string_bytes(name) :: args.toList)
   6.204 +    command_input._2 ! Input_Chunks(Standard_System.string_bytes(name) :: args.toList)
   6.205  
   6.206    def input(name: String, args: String*): Unit =
   6.207      input_bytes(name, args.map(Standard_System.string_bytes): _*)

     7.1 --- a/src/Pure/System/session.scala	Wed Sep 22 12:52:35 2010 +0200
     7.2 +++ b/src/Pure/System/session.scala	Wed Sep 22 13:47:48 2010 +0200
     7.3 @@ -241,7 +241,7 @@
     7.4            Some(startup_error())
     7.5  
     7.6          case TIMEOUT =>  // FIXME clarify
     7.7 -          prover.kill; Some(startup_error())
     7.8 +          prover.terminate; Some(startup_error())
     7.9        }
    7.10      }
    7.11  
    7.12 @@ -282,7 +282,7 @@
    7.13          case Stop => // FIXME synchronous!?
    7.14            if (prover != null) {
    7.15              global_state.change(_ => Document.State.init)
    7.16 -            prover.kill
    7.17 +            prover.terminate
    7.18              prover = null
    7.19            }
    7.20