distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
authorwenzelm
Tue Aug 10 12:29:11 2010 +0200 (2010-08-10 ago)
changeset 382592b61c5e27399
parent 38258 dd7dcb9b2637
child 38260 d4a1c7a19be3
distinguish proper Isabelle_Process INPUT vs. raw STDIN, tuned corresponding method names;
asynchronous Isabelle_Process.init -- raw ML toplevel stays active;
simplified Isabelle_Process using actors;
misc tuning;
src/Pure/General/markup.scala
src/Pure/Isar/isar_document.scala
src/Pure/System/isabelle_process.ML
src/Pure/System/isabelle_process.scala
     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 -
    4.37 -  private def output_raw(text: String) = synchronized {
    4.38 -    if (proc == null) error("Cannot output to Isabelle: no process")
    4.39 -    if (closing) error("Cannot output to Isabelle: already closing")
    4.40 -    output.put(text)
    4.41 -  }
    4.42  
    4.43 -  def output_sync(text: String) =
    4.44 -    output_raw(" \\<^sync>\n; " + text + " \\<^sync>;\n")
    4.45 -
    4.46 -
    4.47 -  def command(text: String) =
    4.48 -    output_sync("Isabelle.command " + Isabelle_Syntax.encode_string(text))
    4.49 +  /** stream actors **/
    4.50  
    4.51 -  def command(props: List[(String, String)], text: String) =
    4.52 -    output_sync("Isabelle.command " + Isabelle_Syntax.encode_properties(props) + " " +
    4.53 -      Isabelle_Syntax.encode_string(text))
    4.54 -
    4.55 -  def ML_val(text: String) =
    4.56 -    output_sync("ML_val " + Isabelle_Syntax.encode_string(text))
    4.57 +  /* input */
    4.58  
    4.59 -  def ML_command(text: String) =
    4.60 -    output_sync("ML_command " + Isabelle_Syntax.encode_string(text))
    4.61 -
    4.62 -  def close() = synchronized {    // FIXME watchdog/timeout
    4.63 -    output_raw("\u0000")
    4.64 -    closing = true
    4.65 -  }
    4.66 +  case class Input(cmd: String)
    4.67 +  case object Close
    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  
   4.185 -  /** main **/
   4.186 +  /** init **/
   4.187 +
   4.188 +  /* exec process */
   4.189  
   4.190 -  {
   4.191 -    /* private communication channels */
   4.192 +  private val in_fifo = system.mk_fifo()
   4.193 +  private val out_fifo = system.mk_fifo()
   4.194 +  private def rm_fifos() = { system.rm_fifo(in_fifo); system.rm_fifo(out_fifo) }
   4.195  
   4.196 -    val in_fifo = system.mk_fifo()
   4.197 -    val out_fifo = system.mk_fifo()
   4.198 -    def rm_fifos() = { system.rm_fifo(in_fifo); system.rm_fifo(out_fifo) }
   4.199 +  try {
   4.200 +    val cmdline =
   4.201 +      List(system.getenv_strict("ISABELLE_PROCESS"), "-W", in_fifo + ":" + out_fifo) ++ args
   4.202 +    proc = system.execute(true, cmdline: _*)
   4.203 +  }
   4.204 +  catch {
   4.205 +    case e: IOException =>
   4.206 +      rm_fifos()
   4.207 +      error("Failed to execute Isabelle process: " + e.getMessage)
   4.208 +  }
   4.209  
   4.210 -    val command_thread = new Command_Thread(in_fifo)
   4.211 -    val message_thread = new Message_Thread(out_fifo)
   4.212 +
   4.213 +  /* exit process */
   4.214  
   4.215 -    command_thread.start
   4.216 -    message_thread.start
   4.217 +  Library.thread_actor("process_exit") {
   4.218 +    val rc = proc.waitFor()
   4.219 +    Thread.sleep(300)  // FIXME property!?
   4.220 +    put_result(Markup.SYSTEM, "process_exit terminated")
   4.221 +    put_result(Markup.EXIT, rc.toString)
   4.222 +    rm_fifos()
   4.223 +  }
   4.224  
   4.225  
   4.226 -    /* exec process */
   4.227 +  /* I/O actors */
   4.228 +
   4.229 +  private val standard_input =
   4.230 +    input_actor("standard_input", Markup.STDIN, proc.getOutputStream)
   4.231  
   4.232 -    try {
   4.233 -      val cmdline =
   4.234 -        List(system.getenv_strict("ISABELLE_PROCESS"), "-W", in_fifo + ":" + out_fifo) ++ args
   4.235 -      proc = system.execute(true, cmdline: _*)
   4.236 -    }
   4.237 -    catch {
   4.238 -      case e: IOException =>
   4.239 -        rm_fifos()
   4.240 -        error("Failed to execute Isabelle process: " + e.getMessage)
   4.241 -    }
   4.242 -    new Stdout_Thread(proc.getInputStream).start
   4.243 +  private val command_input =
   4.244 +    input_actor("command_input", Markup.INPUT, system.fifo_output_stream(in_fifo))
   4.245 +
   4.246 +  output_actor("standard_output", Markup.STDOUT, proc.getInputStream)
   4.247 +  message_actor("message_output", system.fifo_input_stream(out_fifo))
   4.248 +
   4.249  
   4.250  
   4.251 -    /* exit */
   4.252 +  /** main methods **/
   4.253 +
   4.254 +  def input_raw(text: String) = standard_input ! Input(text)
   4.255 +
   4.256 +  def input(text: String) = synchronized {  // FIXME avoid synchronized
   4.257 +    if (proc == null) error("Cannot output to Isabelle: no process")
   4.258 +    if (closing) error("Cannot output to Isabelle: already closing")
   4.259 +    command_input ! Input(" \\<^sync>\n; " + text + " \\<^sync>;\n")
   4.260 +  }
   4.261 +
   4.262 +  def command(text: String) = input("Isabelle.command " + Isabelle_Syntax.encode_string(text))
   4.263  
   4.264 -    new Thread("isabelle: exit") {
   4.265 -      override def run()
   4.266 -      {
   4.267 -        val rc = proc.waitFor()
   4.268 -        Thread.sleep(300)  // FIXME property!?
   4.269 -        put_result(Markup.SYSTEM, "Exit thread terminated")
   4.270 -        put_result(Markup.EXIT, rc.toString)
   4.271 -        rm_fifos()
   4.272 -      }
   4.273 -    }.start
   4.274 +  def command(props: List[(String, String)], text: String) =
   4.275 +    input("Isabelle.command " + Isabelle_Syntax.encode_properties(props) + " " +
   4.276 +      Isabelle_Syntax.encode_string(text))
   4.277 +
   4.278 +  def ML_val(text: String) = input("ML_val " + Isabelle_Syntax.encode_string(text))
   4.279 +  def ML_command(text: String) = input("ML_command " + Isabelle_Syntax.encode_string(text))
   4.280 +
   4.281 +  def close() = synchronized {    // FIXME avoid synchronized
   4.282 +    command_input ! Close
   4.283 +    closing = true
   4.284 +  }
   4.285 +
   4.286 +  def try_close() = synchronized {
   4.287 +    if (proc != null && !closing) {
   4.288 +      try { close() }
   4.289 +      catch { case _: RuntimeException => }
   4.290 +    }
   4.291    }
   4.292  }