1.1 --- a/src/Pure/General/markup.scala	Tue Aug 10 12:09:53 2010 +0200
     1.2 +++ b/src/Pure/General/markup.scala	Tue Aug 10 12:29:11 2010 +0200
     1.3 @@ -203,6 +203,7 @@
     1.4    val ERROR = "error"
     1.5    val DEBUG = "debug"
     1.6    val SYSTEM = "system"
     1.7 +  val INPUT = "input"
     1.8    val STDIN = "stdin"
     1.9    val STDOUT = "stdout"
    1.10    val SIGNAL = "signal"

     2.1 --- a/src/Pure/Isar/isar_document.scala	Tue Aug 10 12:09:53 2010 +0200
     2.2 +++ b/src/Pure/Isar/isar_document.scala	Tue Aug 10 12:29:11 2010 +0200
     2.3 @@ -38,7 +38,7 @@
     2.4    /* commands */
     2.5  
     2.6    def define_command(id: Document.Command_ID, text: String) {
     2.7 -    output_sync("Isar.define_command " + Isabelle_Syntax.encode_string(id) + " " +
     2.8 +    input("Isar.define_command " + Isabelle_Syntax.encode_string(id) + " " +
     2.9        Isabelle_Syntax.encode_string(text))
    2.10    }
    2.11  
    2.12 @@ -80,6 +80,6 @@
    2.13      Isabelle_Syntax.append_string(new_id, buf)
    2.14      buf.append(" ")
    2.15      Isabelle_Syntax.append_list(append_node_edit, edits, buf)
    2.16 -    output_sync(buf.toString)
    2.17 +    input(buf.toString)
    2.18    }
    2.19  }

     3.1 --- a/src/Pure/System/isabelle_process.ML	Tue Aug 10 12:09:53 2010 +0200
     3.2 +++ b/src/Pure/System/isabelle_process.ML	Tue Aug 10 12:29:11 2010 +0200
     3.3 @@ -105,6 +105,10 @@
     3.4      val _ = quick_and_dirty := true;  (* FIXME !? *)
     3.5      val _ = Keyword.status ();
     3.6      val _ = Output.status (Markup.markup Markup.ready "");
     3.7 -  in Isar.toplevel_loop in_stream {init = true, welcome = false, sync = true, secure = true} end;
     3.8 +    val _ =
     3.9 +      Simple_Thread.fork false (fn () =>
    3.10 +        (Isar.toplevel_loop in_stream {init = true, welcome = false, sync = true, secure = true};
    3.11 +          quit ()));
    3.12 +  in () end;
    3.13  
    3.14  end;

     4.1 --- a/src/Pure/System/isabelle_process.scala	Tue Aug 10 12:09:53 2010 +0200
     4.2 +++ b/src/Pure/System/isabelle_process.scala	Tue Aug 10 12:29:11 2010 +0200
     4.3 @@ -38,6 +38,7 @@
     4.4        kind == Markup.EXIT
     4.5      def is_system(kind: String) =
     4.6        kind == Markup.SYSTEM ||
     4.7 +      kind == Markup.INPUT ||
     4.8        kind == Markup.STDIN ||
     4.9        kind == Markup.SIGNAL ||
    4.10        kind == Markup.EXIT ||
    4.11 @@ -111,7 +112,7 @@
    4.12  
    4.13    /* signals */
    4.14  
    4.15 -  def interrupt() = synchronized {
    4.16 +  def interrupt() = synchronized {  // FIXME avoid synchronized
    4.17      if (proc == null) error("Cannot interrupt Isabelle: no process")
    4.18      if (pid == null) put_result(Markup.SYSTEM, "Cannot interrupt: unknown pid")
    4.19      else {
    4.20 @@ -125,7 +126,7 @@
    4.21      }
    4.22    }
    4.23  
    4.24 -  def kill() = synchronized {
    4.25 +  def kill() = synchronized {  // FIXME avoid synchronized
    4.26      if (proc == 0) error("Cannot kill Isabelle: no process")
    4.27      else {
    4.28        try_close()
    4.29 @@ -138,85 +139,45 @@
    4.30    }
    4.31  
    4.32  
    4.33 -  /* output being piped into the process */
    4.34  
    4.35 -  private val output = new LinkedBlockingQueue[String]
    4.36 +  /** stream actors **/
    4.37  
    4.38 -  private def output_raw(text: String) = synchronized {
    4.39 -    if (proc == null) error("Cannot output to Isabelle: no process")
    4.40 -    if (closing) error("Cannot output to Isabelle: already closing")
    4.41 -    output.put(text)
    4.42 -  }
    4.43 +  /* input */
    4.44  
    4.45 -  def output_sync(text: String) =
    4.46 -    output_raw(" \\<^sync>\n; " + text + " \\<^sync>;\n")
    4.47 +  case class Input(cmd: String)
    4.48 +  case object Close
    4.49  
    4.50 -
    4.51 -  def command(text: String) =
    4.52 -    output_sync("Isabelle.command " + Isabelle_Syntax.encode_string(text))
    4.53 -
    4.54 -  def command(props: List[(String, String)], text: String) =
    4.55 -    output_sync("Isabelle.command " + Isabelle_Syntax.encode_properties(props) + " " +
    4.56 -      Isabelle_Syntax.encode_string(text))
    4.57 -
    4.58 -  def ML_val(text: String) =
    4.59 -    output_sync("ML_val " + Isabelle_Syntax.encode_string(text))
    4.60 -
    4.61 -  def ML_command(text: String) =
    4.62 -    output_sync("ML_command " + Isabelle_Syntax.encode_string(text))
    4.63 -
    4.64 -  def close() = synchronized {    // FIXME watchdog/timeout
    4.65 -    output_raw("\u0000")
    4.66 -    closing = true
    4.67 -  }
    4.68 -
    4.69 -  def try_close() = synchronized {
    4.70 -    if (proc != null && !closing) {
    4.71 -      try { close() }
    4.72 -      catch { case _: RuntimeException => }
    4.73 -    }
    4.74 -  }
    4.75 -
    4.76 -
    4.77 -  /* commands */
    4.78 -
    4.79 -  private class Command_Thread(fifo: String) extends Thread("isabelle: commands")
    4.80 -  {
    4.81 -    override def run()
    4.82 -    {
    4.83 -      val stream = system.fifo_output_stream(fifo)
    4.84 +  private def input_actor(name: String, kind: String, stream: => OutputStream): Actor =
    4.85 +    Library.thread_actor(name) {
    4.86        val writer = new BufferedWriter(new OutputStreamWriter(stream, Standard_System.charset))
    4.87        var finished = false
    4.88        while (!finished) {
    4.89          try {
    4.90            //{{{
    4.91 -          val s = output.take
    4.92 -          if (s == "\u0000") {
    4.93 -            writer.close
    4.94 -            finished = true
    4.95 -          }
    4.96 -          else {
    4.97 -            put_result(Markup.STDIN, s)
    4.98 -            writer.write(s)
    4.99 -            writer.flush
   4.100 +          receive {
   4.101 +            case Input(text) =>
   4.102 +              put_result(kind, text)
   4.103 +              writer.write(text)
   4.104 +              writer.flush
   4.105 +            case Close =>
   4.106 +              writer.close
   4.107 +              finished = true
   4.108 +            case bad => System.err.println(name + ": ignoring bad message " + bad)
   4.109            }
   4.110            //}}}
   4.111          }
   4.112          catch {
   4.113 -          case e: IOException => put_result(Markup.SYSTEM, "Command thread: " + e.getMessage)
   4.114 +          case e: IOException => put_result(Markup.SYSTEM, name + ": " + e.getMessage)
   4.115          }
   4.116        }
   4.117 -      put_result(Markup.SYSTEM, "Command thread terminated")
   4.118 +      put_result(Markup.SYSTEM, name + " terminated")
   4.119      }
   4.120 -  }
   4.121  
   4.122  
   4.123 -  /* raw stdout */
   4.124 +  /* raw output */
   4.125  
   4.126 -  private class Stdout_Thread(stream: InputStream) extends Thread("isabelle: stdout")
   4.127 -  {
   4.128 -    override def run() =
   4.129 -    {
   4.130 +  private def output_actor(name: String, kind: String, stream: => InputStream): Actor =
   4.131 +    Library.thread_actor(name) {
   4.132        val reader = new BufferedReader(new InputStreamReader(stream, Standard_System.charset))
   4.133        var result = new StringBuilder(100)
   4.134  
   4.135 @@ -232,7 +193,7 @@
   4.136              else done = true
   4.137            }
   4.138            if (result.length > 0) {
   4.139 -            put_result(Markup.STDOUT, result.toString)
   4.140 +            put_result(kind, result.toString)
   4.141              result.length = 0
   4.142            }
   4.143            else {
   4.144 @@ -243,22 +204,19 @@
   4.145            //}}}
   4.146          }
   4.147          catch {
   4.148 -          case e: IOException => put_result(Markup.SYSTEM, "Stdout thread: " + e.getMessage)
   4.149 +          case e: IOException => put_result(Markup.SYSTEM, name + ": " + e.getMessage)
   4.150          }
   4.151        }
   4.152 -      put_result(Markup.SYSTEM, "Stdout thread terminated")
   4.153 +      put_result(Markup.SYSTEM, name + " terminated")
   4.154      }
   4.155 -  }
   4.156  
   4.157  
   4.158 -  /* messages */
   4.159 +  /* message output */
   4.160  
   4.161 -  private class Message_Thread(fifo: String) extends Thread("isabelle: messages")
   4.162 -  {
   4.163 -    private class Protocol_Error(msg: String) extends Exception(msg)
   4.164 -    override def run()
   4.165 -    {
   4.166 -      val stream = system.fifo_input_stream(fifo)
   4.167 +  private class Protocol_Error(msg: String) extends Exception(msg)
   4.168 +
   4.169 +  private def message_actor(name: String, stream: InputStream): Actor =
   4.170 +    Library.thread_actor(name) {
   4.171        val default_buffer = new Array[Byte](65536)
   4.172        var c = -1
   4.173  
   4.174 @@ -325,54 +283,83 @@
   4.175        stream.close
   4.176        try_close()
   4.177  
   4.178 -      put_result(Markup.SYSTEM, "Message thread terminated")
   4.179 +      put_result(Markup.SYSTEM, name + " terminated")
   4.180 +    }
   4.181 +
   4.182 +
   4.183 +
   4.184 +  /** init **/
   4.185 +
   4.186 +  /* exec process */
   4.187 +
   4.188 +  private val in_fifo = system.mk_fifo()
   4.189 +  private val out_fifo = system.mk_fifo()
   4.190 +  private def rm_fifos() = { system.rm_fifo(in_fifo); system.rm_fifo(out_fifo) }
   4.191 +
   4.192 +  try {
   4.193 +    val cmdline =
   4.194 +      List(system.getenv_strict("ISABELLE_PROCESS"), "-W", in_fifo + ":" + out_fifo) ++ args
   4.195 +    proc = system.execute(true, cmdline: _*)
   4.196 +  }
   4.197 +  catch {
   4.198 +    case e: IOException =>
   4.199 +      rm_fifos()
   4.200 +      error("Failed to execute Isabelle process: " + e.getMessage)
   4.201 +  }
   4.202 +
   4.203 +
   4.204 +  /* exit process */
   4.205 +
   4.206 +  Library.thread_actor("process_exit") {
   4.207 +    val rc = proc.waitFor()
   4.208 +    Thread.sleep(300)  // FIXME property!?
   4.209 +    put_result(Markup.SYSTEM, "process_exit terminated")
   4.210 +    put_result(Markup.EXIT, rc.toString)
   4.211 +    rm_fifos()
   4.212 +  }
   4.213 +
   4.214 +
   4.215 +  /* I/O actors */
   4.216 +
   4.217 +  private val standard_input =
   4.218 +    input_actor("standard_input", Markup.STDIN, proc.getOutputStream)
   4.219 +
   4.220 +  private val command_input =
   4.221 +    input_actor("command_input", Markup.INPUT, system.fifo_output_stream(in_fifo))
   4.222 +
   4.223 +  output_actor("standard_output", Markup.STDOUT, proc.getInputStream)
   4.224 +  message_actor("message_output", system.fifo_input_stream(out_fifo))
   4.225 +
   4.226 +
   4.227 +
   4.228 +  /** main methods **/
   4.229 +
   4.230 +  def input_raw(text: String) = standard_input ! Input(text)
   4.231 +
   4.232 +  def input(text: String) = synchronized {  // FIXME avoid synchronized
   4.233 +    if (proc == null) error("Cannot output to Isabelle: no process")
   4.234 +    if (closing) error("Cannot output to Isabelle: already closing")
   4.235 +    command_input ! Input(" \\<^sync>\n; " + text + " \\<^sync>;\n")
   4.236 +  }
   4.237 +
   4.238 +  def command(text: String) = input("Isabelle.command " + Isabelle_Syntax.encode_string(text))
   4.239 +
   4.240 +  def command(props: List[(String, String)], text: String) =
   4.241 +    input("Isabelle.command " + Isabelle_Syntax.encode_properties(props) + " " +
   4.242 +      Isabelle_Syntax.encode_string(text))
   4.243 +
   4.244 +  def ML_val(text: String) = input("ML_val " + Isabelle_Syntax.encode_string(text))
   4.245 +  def ML_command(text: String) = input("ML_command " + Isabelle_Syntax.encode_string(text))
   4.246 +
   4.247 +  def close() = synchronized {    // FIXME avoid synchronized
   4.248 +    command_input ! Close
   4.249 +    closing = true
   4.250 +  }
   4.251 +
   4.252 +  def try_close() = synchronized {
   4.253 +    if (proc != null && !closing) {
   4.254 +      try { close() }
   4.255 +      catch { case _: RuntimeException => }
   4.256      }
   4.257    }
   4.258 -
   4.259 -
   4.260 -
   4.261 -  /** main **/
   4.262 -
   4.263 -  {
   4.264 -    /* private communication channels */
   4.265 -
   4.266 -    val in_fifo = system.mk_fifo()
   4.267 -    val out_fifo = system.mk_fifo()
   4.268 -    def rm_fifos() = { system.rm_fifo(in_fifo); system.rm_fifo(out_fifo) }
   4.269 -
   4.270 -    val command_thread = new Command_Thread(in_fifo)
   4.271 -    val message_thread = new Message_Thread(out_fifo)
   4.272 -
   4.273 -    command_thread.start
   4.274 -    message_thread.start
   4.275 -
   4.276 -
   4.277 -    /* exec process */
   4.278 -
   4.279 -    try {
   4.280 -      val cmdline =
   4.281 -        List(system.getenv_strict("ISABELLE_PROCESS"), "-W", in_fifo + ":" + out_fifo) ++ args
   4.282 -      proc = system.execute(true, cmdline: _*)
   4.283 -    }
   4.284 -    catch {
   4.285 -      case e: IOException =>
   4.286 -        rm_fifos()
   4.287 -        error("Failed to execute Isabelle process: " + e.getMessage)
   4.288 -    }
   4.289 -    new Stdout_Thread(proc.getInputStream).start
   4.290 -
   4.291 -
   4.292 -    /* exit */
   4.293 -
   4.294 -    new Thread("isabelle: exit") {
   4.295 -      override def run()
   4.296 -      {
   4.297 -        val rc = proc.waitFor()
   4.298 -        Thread.sleep(300)  // FIXME property!?
   4.299 -        put_result(Markup.SYSTEM, "Exit thread terminated")
   4.300 -        put_result(Markup.EXIT, rc.toString)
   4.301 -        rm_fifos()
   4.302 -      }
   4.303 -    }.start
   4.304 -  }
   4.305  }