src/Pure/System/isabelle_process.scala
changeset 38270 71bb3c273dd1
parent 38262 bb2df73fab2c
child 38372 e753f71b6b34
     1.1 --- a/src/Pure/System/isabelle_process.scala	Wed Aug 11 00:42:40 2010 +0200
     1.2 +++ b/src/Pure/System/isabelle_process.scala	Wed Aug 11 00:44:48 2010 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  
     1.5  import java.util.concurrent.LinkedBlockingQueue
     1.6  import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter,
     1.7 -  InputStream, OutputStream, IOException}
     1.8 +  InputStream, OutputStream, BufferedOutputStream, IOException}
     1.9  
    1.10  import scala.actors.Actor
    1.11  import Actor._
    1.12 @@ -89,9 +89,8 @@
    1.13  
    1.14    /* process information */
    1.15  
    1.16 -  @volatile private var proc: Process = null
    1.17 -  @volatile private var closing = false
    1.18 -  @volatile private var pid: String = null
    1.19 +  @volatile private var proc: Option[Process] = None
    1.20 +  @volatile private var pid: Option[String] = None
    1.21  
    1.22  
    1.23    /* results */
    1.24 @@ -99,7 +98,7 @@
    1.25    private def put_result(kind: String, props: List[(String, String)], body: List[XML.Tree])
    1.26    {
    1.27      if (kind == Markup.INIT) {
    1.28 -      for ((Markup.PID, p) <- props) pid = p
    1.29 +      for ((Markup.PID, p) <- props) pid = Some(p)
    1.30      }
    1.31      receiver ! new Result(XML.Elem(Markup(kind, props), body))
    1.32    }
    1.33 @@ -112,29 +111,34 @@
    1.34  
    1.35    /* signals */
    1.36  
    1.37 -  def interrupt() = synchronized {  // FIXME avoid synchronized
    1.38 -    if (proc == null) error("Cannot interrupt Isabelle: no process")
    1.39 -    if (pid == null) put_result(Markup.SYSTEM, "Cannot interrupt: unknown pid")
    1.40 -    else {
    1.41 -      try {
    1.42 -        if (system.execute(true, "kill", "-INT", pid).waitFor == 0)
    1.43 -          put_result(Markup.SIGNAL, "INT")
    1.44 -        else
    1.45 -          put_result(Markup.SYSTEM, "Cannot interrupt: kill command failed")
    1.46 +  def interrupt()
    1.47 +  {
    1.48 +    if (proc.isEmpty) put_result(Markup.SYSTEM, "Cannot interrupt Isabelle: no process")
    1.49 +    else
    1.50 +      pid match {
    1.51 +        case None => put_result(Markup.SYSTEM, "Cannot interrupt Isabelle: unknowd pid")
    1.52 +        case Some(i) =>
    1.53 +          try {
    1.54 +            if (system.execute(true, "kill", "-INT", i).waitFor == 0)
    1.55 +              put_result(Markup.SIGNAL, "INT")
    1.56 +            else
    1.57 +              put_result(Markup.SYSTEM, "Cannot interrupt Isabelle: kill command failed")
    1.58 +          }
    1.59 +          catch { case e: IOException => error("Cannot interrupt Isabelle: " + e.getMessage) }
    1.60        }
    1.61 -      catch { case e: IOException => error("Cannot interrupt Isabelle: " + e.getMessage) }
    1.62 -    }
    1.63    }
    1.64  
    1.65 -  def kill() = synchronized {  // FIXME avoid synchronized
    1.66 -    if (proc == 0) error("Cannot kill Isabelle: no process")
    1.67 -    else {
    1.68 -      try_close()
    1.69 -      Thread.sleep(500)  // FIXME property!?
    1.70 -      put_result(Markup.SIGNAL, "KILL")
    1.71 -      proc.destroy
    1.72 -      proc = null
    1.73 -      pid = null
    1.74 +  def kill()
    1.75 +  {
    1.76 +    proc match {
    1.77 +      case None => put_result(Markup.SYSTEM, "Cannot kill Isabelle: no process")
    1.78 +      case Some(p) =>
    1.79 +        close()
    1.80 +        Thread.sleep(500)  // FIXME !?
    1.81 +        put_result(Markup.SIGNAL, "KILL")
    1.82 +        p.destroy
    1.83 +        proc = None
    1.84 +        pid = None
    1.85      }
    1.86    }
    1.87  
    1.88 @@ -142,12 +146,14 @@
    1.89  
    1.90    /** stream actors **/
    1.91  
    1.92 -  /* input */
    1.93 -
    1.94 -  case class Input(cmd: String)
    1.95 +  case class Input_Text(text: String)
    1.96 +  case class Input_Chunks(chunks: List[Array[Byte]])
    1.97    case object Close
    1.98  
    1.99 -  private def input_actor(name: String, kind: String, stream: => OutputStream): Actor =
   1.100 +
   1.101 +  /* raw stdin */
   1.102 +
   1.103 +  private def stdin_actor(name: String, stream: OutputStream): Actor =
   1.104      Library.thread_actor(name) {
   1.105        val writer = new BufferedWriter(new OutputStreamWriter(stream, Standard_System.charset))
   1.106        var finished = false
   1.107 @@ -155,8 +161,8 @@
   1.108          try {
   1.109            //{{{
   1.110            receive {
   1.111 -            case Input(text) =>
   1.112 -              put_result(kind, text)
   1.113 +            case Input_Text(text) =>
   1.114 +              // FIXME echo input?!
   1.115                writer.write(text)
   1.116                writer.flush
   1.117              case Close =>
   1.118 @@ -174,9 +180,9 @@
   1.119      }
   1.120  
   1.121  
   1.122 -  /* raw output */
   1.123 +  /* raw stdout */
   1.124  
   1.125 -  private def output_actor(name: String, kind: String, stream: => InputStream): Actor =
   1.126 +  private def stdout_actor(name: String, stream: InputStream): Actor =
   1.127      Library.thread_actor(name) {
   1.128        val reader = new BufferedReader(new InputStreamReader(stream, Standard_System.charset))
   1.129        var result = new StringBuilder(100)
   1.130 @@ -193,13 +199,43 @@
   1.131              else done = true
   1.132            }
   1.133            if (result.length > 0) {
   1.134 -            put_result(kind, result.toString)
   1.135 +            put_result(Markup.STDOUT, result.toString)
   1.136              result.length = 0
   1.137            }
   1.138            else {
   1.139              reader.close
   1.140              finished = true
   1.141 -            try_close()
   1.142 +            close()
   1.143 +          }
   1.144 +          //}}}
   1.145 +        }
   1.146 +        catch {
   1.147 +          case e: IOException => put_result(Markup.SYSTEM, name + ": " + e.getMessage)
   1.148 +        }
   1.149 +      }
   1.150 +      put_result(Markup.SYSTEM, name + " terminated")
   1.151 +    }
   1.152 +
   1.153 +
   1.154 +  /* command input */
   1.155 +
   1.156 +  private def input_actor(name: String, raw_stream: OutputStream): Actor =
   1.157 +    Library.thread_actor(name) {
   1.158 +      val stream = new BufferedOutputStream(raw_stream)
   1.159 +      var finished = false
   1.160 +      while (!finished) {
   1.161 +        try {
   1.162 +          //{{{
   1.163 +          receive {
   1.164 +            case Input_Chunks(chunks) =>
   1.165 +              stream.write(Standard_System.string_bytes(
   1.166 +                  chunks.map(_.length).mkString("", ",", "\n")));
   1.167 +              chunks.foreach(stream.write(_));
   1.168 +              stream.flush
   1.169 +            case Close =>
   1.170 +              stream.close
   1.171 +              finished = true
   1.172 +            case bad => System.err.println(name + ": ignoring bad message " + bad)
   1.173            }
   1.174            //}}}
   1.175          }
   1.176 @@ -281,7 +317,7 @@
   1.177          }
   1.178        } while (c != -1)
   1.179        stream.close
   1.180 -      try_close()
   1.181 +      close()
   1.182  
   1.183        put_result(Markup.SYSTEM, name + " terminated")
   1.184      }
   1.185 @@ -299,7 +335,7 @@
   1.186    try {
   1.187      val cmdline =
   1.188        List(system.getenv_strict("ISABELLE_PROCESS"), "-W", in_fifo + ":" + out_fifo) ++ args
   1.189 -    proc = system.execute(true, cmdline: _*)
   1.190 +    proc = Some(system.execute(true, cmdline: _*))
   1.191    }
   1.192    catch {
   1.193      case e: IOException =>
   1.194 @@ -308,49 +344,37 @@
   1.195    }
   1.196  
   1.197  
   1.198 +  /* I/O actors */
   1.199 +
   1.200 +  private val standard_input = stdin_actor("standard_input", proc.get.getOutputStream)
   1.201 +  stdout_actor("standard_output", proc.get.getInputStream)
   1.202 +
   1.203 +  private val command_input = input_actor("command_input", system.fifo_output_stream(in_fifo))
   1.204 +  message_actor("message_output", system.fifo_input_stream(out_fifo))
   1.205 +
   1.206 +
   1.207    /* exit process */
   1.208  
   1.209    Library.thread_actor("process_exit") {
   1.210 -    val rc = proc.waitFor()
   1.211 -    Thread.sleep(300)  // FIXME property!?
   1.212 -    put_result(Markup.SYSTEM, "process_exit terminated")
   1.213 -    put_result(Markup.EXIT, rc.toString)
   1.214 +    proc match {
   1.215 +      case None =>
   1.216 +      case Some(p) =>
   1.217 +        val rc = p.waitFor()
   1.218 +        Thread.sleep(300)  // FIXME property!?
   1.219 +        put_result(Markup.SYSTEM, "process_exit terminated")
   1.220 +        put_result(Markup.EXIT, rc.toString)
   1.221 +    }
   1.222      rm_fifos()
   1.223    }
   1.224  
   1.225  
   1.226 -  /* I/O actors */
   1.227 -
   1.228 -  private val standard_input =
   1.229 -    input_actor("standard_input", Markup.STDIN, proc.getOutputStream)
   1.230 -
   1.231 -  private val command_input =
   1.232 -    input_actor("command_input", Markup.INPUT, system.fifo_output_stream(in_fifo))
   1.233 -
   1.234 -  output_actor("standard_output", Markup.STDOUT, proc.getInputStream)
   1.235 -  message_actor("message_output", system.fifo_input_stream(out_fifo))
   1.236 -
   1.237 -
   1.238  
   1.239    /** main methods **/
   1.240  
   1.241 -  def input_raw(text: String) = standard_input ! Input(text)
   1.242 -
   1.243 -  def input(text: String) = synchronized {  // FIXME avoid synchronized
   1.244 -    if (proc == null) error("Cannot output to Isabelle: no process")
   1.245 -    if (closing) error("Cannot output to Isabelle: already closing")
   1.246 -    command_input ! Input(" \\<^sync>\n; " + text + " \\<^sync>;\n")
   1.247 -  }
   1.248 +  def input_raw(text: String): Unit = standard_input ! Input_Text(text)
   1.249  
   1.250 -  def close() = synchronized {    // FIXME avoid synchronized
   1.251 -    command_input ! Close
   1.252 -    closing = true
   1.253 -  }
   1.254 +  def input(name: String, args: String*): Unit =
   1.255 +    command_input ! Input_Chunks((name :: args.toList).map(Standard_System.string_bytes))
   1.256  
   1.257 -  def try_close() = synchronized {
   1.258 -    if (proc != null && !closing) {
   1.259 -      try { close() }
   1.260 -      catch { case _: RuntimeException => }
   1.261 -    }
   1.262 -  }
   1.263 +  def close(): Unit = command_input ! Close
   1.264  }