1.1 --- a/src/Pure/System/isabelle_process.scala Thu Dec 17 20:09:19 2009 +0100
1.2 +++ b/src/Pure/System/isabelle_process.scala Thu Dec 17 20:14:00 2009 +0100
1.3 @@ -82,12 +82,15 @@
1.4 kind == STATUS
1.5 }
1.6
1.7 - class Result(val kind: Kind.Value, val props: List[(String, String)], val result: String) {
1.8 - override def toString = {
1.9 - val trees = YXML.parse_body_failsafe(result)
1.10 + class Result(val kind: Kind.Value, val props: List[(String, String)], val body: List[XML.Tree])
1.11 + {
1.12 + def message = XML.Elem(Markup.MESSAGE, (Markup.CLASS, Kind.markup(kind)) :: props, body)
1.13 +
1.14 + override def toString: String =
1.15 + {
1.16 val res =
1.17 - if (kind == Kind.STATUS) trees.map(_.toString).mkString
1.18 - else trees.flatMap(XML.content(_).mkString).mkString
1.19 + if (kind == Kind.STATUS) body.map(_.toString).mkString
1.20 + else body.map(XML.content(_).mkString).mkString
1.21 if (props.isEmpty)
1.22 kind.toString + " [[" + res + "]]"
1.23 else
1.24 @@ -98,16 +101,10 @@
1.25 def is_control = Kind.is_control(kind)
1.26 def is_system = Kind.is_system(kind)
1.27 }
1.28 -
1.29 - def parse_message(isabelle_system: Isabelle_System, result: Result) =
1.30 - {
1.31 - XML.Elem(Markup.MESSAGE, (Markup.CLASS, Kind.markup(result.kind)) :: result.props,
1.32 - YXML.parse_body_failsafe(isabelle_system.symbols.decode(result.result)))
1.33 - }
1.34 }
1.35
1.36
1.37 -class Isabelle_Process(isabelle_system: Isabelle_System, receiver: Actor, args: String*)
1.38 +class Isabelle_Process(system: Isabelle_System, receiver: Actor, args: String*)
1.39 {
1.40 import Isabelle_Process._
1.41
1.42 @@ -130,14 +127,19 @@
1.43
1.44 /* results */
1.45
1.46 - private def put_result(kind: Kind.Value, props: List[(String, String)], result: String)
1.47 + private def put_result(kind: Kind.Value, props: List[(String, String)], body: List[XML.Tree])
1.48 {
1.49 if (kind == Kind.INIT) {
1.50 val map = Map(props: _*)
1.51 if (map.isDefinedAt(Markup.PID)) pid = map(Markup.PID)
1.52 if (map.isDefinedAt(Markup.SESSION)) the_session = map(Markup.SESSION)
1.53 }
1.54 - receiver ! new Result(kind, props, result)
1.55 + receiver ! new Result(kind, props, body)
1.56 + }
1.57 +
1.58 + private def put_result(kind: Kind.Value, text: String)
1.59 + {
1.60 + put_result(kind, Nil, List(XML.Text(system.symbols.decode(text))))
1.61 }
1.62
1.63
1.64 @@ -145,13 +147,13 @@
1.65
1.66 def interrupt() = synchronized {
1.67 if (proc == null) error("Cannot interrupt Isabelle: no process")
1.68 - if (pid == null) put_result(Kind.SYSTEM, Nil, "Cannot interrupt: unknown pid")
1.69 + if (pid == null) put_result(Kind.SYSTEM, "Cannot interrupt: unknown pid")
1.70 else {
1.71 try {
1.72 - if (isabelle_system.execute(true, "kill", "-INT", pid).waitFor == 0)
1.73 - put_result(Kind.SIGNAL, Nil, "INT")
1.74 + if (system.execute(true, "kill", "-INT", pid).waitFor == 0)
1.75 + put_result(Kind.SIGNAL, "INT")
1.76 else
1.77 - put_result(Kind.SYSTEM, Nil, "Cannot interrupt: kill command failed")
1.78 + put_result(Kind.SYSTEM, "Cannot interrupt: kill command failed")
1.79 }
1.80 catch { case e: IOException => error("Cannot interrupt Isabelle: " + e.getMessage) }
1.81 }
1.82 @@ -162,7 +164,7 @@
1.83 else {
1.84 try_close()
1.85 Thread.sleep(500)
1.86 - put_result(Kind.SIGNAL, Nil, "KILL")
1.87 + put_result(Kind.SIGNAL, "KILL")
1.88 proc.destroy
1.89 proc = null
1.90 pid = null
1.91 @@ -222,17 +224,17 @@
1.92 finished = true
1.93 }
1.94 else {
1.95 - put_result(Kind.STDIN, Nil, s)
1.96 + put_result(Kind.STDIN, s)
1.97 writer.write(s)
1.98 writer.flush
1.99 }
1.100 //}}}
1.101 }
1.102 catch {
1.103 - case e: IOException => put_result(Kind.SYSTEM, Nil, "Stdin thread: " + e.getMessage)
1.104 + case e: IOException => put_result(Kind.SYSTEM, "Stdin thread: " + e.getMessage)
1.105 }
1.106 }
1.107 - put_result(Kind.SYSTEM, Nil, "Stdin thread terminated")
1.108 + put_result(Kind.SYSTEM, "Stdin thread terminated")
1.109 }
1.110 }
1.111
1.112 @@ -256,7 +258,7 @@
1.113 else done = true
1.114 }
1.115 if (result.length > 0) {
1.116 - put_result(Kind.STDOUT, Nil, result.toString)
1.117 + put_result(Kind.STDOUT, result.toString)
1.118 result.length = 0
1.119 }
1.120 else {
1.121 @@ -267,91 +269,89 @@
1.122 //}}}
1.123 }
1.124 catch {
1.125 - case e: IOException => put_result(Kind.SYSTEM, Nil, "Stdout thread: " + e.getMessage)
1.126 + case e: IOException => put_result(Kind.SYSTEM, "Stdout thread: " + e.getMessage)
1.127 }
1.128 }
1.129 - put_result(Kind.SYSTEM, Nil, "Stdout thread terminated")
1.130 + put_result(Kind.SYSTEM, "Stdout thread terminated")
1.131 }
1.132 }
1.133
1.134
1.135 /* messages */
1.136
1.137 - private class MessageThread(fifo: String) extends Thread("isabelle: messages") {
1.138 - override def run() = {
1.139 - val reader = isabelle_system.fifo_reader(fifo)
1.140 - var kind: Kind.Value = null
1.141 - var props: List[(String, String)] = Nil
1.142 - var result = new StringBuilder
1.143 + private class MessageThread(fifo: String) extends Thread("isabelle: messages")
1.144 + {
1.145 + private class Protocol_Error(msg: String) extends Exception(msg)
1.146 + override def run()
1.147 + {
1.148 + val stream = system.fifo_stream(fifo)
1.149 + val default_buffer = new Array[Byte](65536)
1.150 + var c = -1
1.151
1.152 - var finished = false
1.153 - while (!finished) {
1.154 + def read_chunk(): List[XML.Tree] =
1.155 + {
1.156 + //{{{
1.157 + // chunk size
1.158 + var n = 0
1.159 + c = stream.read
1.160 + while (48 <= c && c <= 57) {
1.161 + n = 10 * n + (c - 48)
1.162 + c = stream.read
1.163 + }
1.164 + if (c != 10) throw new Protocol_Error("bad message chunk header")
1.165 +
1.166 + // chunk content
1.167 + val buf =
1.168 + if (n <= default_buffer.size) default_buffer
1.169 + else new Array[Byte](n)
1.170 +
1.171 + var i = 0
1.172 + var m = 0
1.173 + do {
1.174 + m = stream.read(buf, i, n - i)
1.175 + i += m
1.176 + } while (m > 0 && n > i)
1.177 +
1.178 + if (i != n) throw new Protocol_Error("bad message chunk content")
1.179 +
1.180 + YXML.parse_body_failsafe(YXML.decode_chars(system.symbols.decode, buf, 0, n))
1.181 + //}}}
1.182 + }
1.183 +
1.184 + do {
1.185 try {
1.186 - if (kind == null) {
1.187 - //{{{ Char mode -- resync
1.188 - var c = -1
1.189 - do {
1.190 - c = reader.read
1.191 - if (c >= 0 && c != 2) result.append(c.asInstanceOf[Char])
1.192 - } while (c >= 0 && c != 2)
1.193 -
1.194 - if (result.length > 0) {
1.195 - put_result(Kind.SYSTEM, Nil, "Malformed message:\n" + result.toString)
1.196 - result.length = 0
1.197 + //{{{
1.198 + c = stream.read
1.199 + var non_sync = 0
1.200 + while (c >= 0 && c != 2) {
1.201 + non_sync += 1
1.202 + c = stream.read
1.203 + }
1.204 + if (non_sync > 0)
1.205 + throw new Protocol_Error("lost synchronization -- skipping " + non_sync + " bytes")
1.206 + if (c == 2) {
1.207 + val header = read_chunk()
1.208 + val body = read_chunk()
1.209 + header match {
1.210 + case List(XML.Elem(name, props, Nil))
1.211 + if name.size == 1 && Kind.code.isDefinedAt(name(0)) =>
1.212 + put_result(Kind.code(name(0)), props, body)
1.213 + case _ => throw new Protocol_Error("bad header: " + header.toString)
1.214 }
1.215 - if (c < 0) {
1.216 - reader.close
1.217 - finished = true
1.218 - try_close()
1.219 - }
1.220 - else {
1.221 - c = reader.read
1.222 - if (Kind.code.isDefinedAt(c)) kind = Kind.code(c)
1.223 - else kind = null
1.224 - }
1.225 - //}}}
1.226 }
1.227 - else {
1.228 - //{{{ Line mode
1.229 - val line = reader.readLine
1.230 - if (line == null) {
1.231 - reader.close
1.232 - finished = true
1.233 - try_close()
1.234 - }
1.235 - else {
1.236 - val len = line.length
1.237 - // property
1.238 - if (line.endsWith("\u0002,")) {
1.239 - val i = line.indexOf('=')
1.240 - if (i > 0) {
1.241 - val name = line.substring(0, i)
1.242 - val value = line.substring(i + 1, len - 2)
1.243 - props = (name, value) :: props
1.244 - }
1.245 - }
1.246 - // last text line
1.247 - else if (line.endsWith("\u0002.")) {
1.248 - result.append(line.substring(0, len - 2))
1.249 - put_result(kind, props.reverse, result.toString)
1.250 - kind = null
1.251 - props = Nil
1.252 - result.length = 0
1.253 - }
1.254 - // text line
1.255 - else {
1.256 - result.append(line)
1.257 - result.append('\n')
1.258 - }
1.259 - }
1.260 - //}}}
1.261 - }
1.262 + //}}}
1.263 }
1.264 catch {
1.265 - case e: IOException => put_result(Kind.SYSTEM, Nil, "Message thread: " + e.getMessage)
1.266 + case e: IOException =>
1.267 + put_result(Kind.SYSTEM, "Cannot read message:\n" + e.getMessage)
1.268 + case e: Protocol_Error =>
1.269 + put_result(Kind.SYSTEM, "Malformed message:\n" + e.getMessage)
1.270 }
1.271 - }
1.272 - put_result(Kind.SYSTEM, Nil, "Message thread terminated")
1.273 + } while (c != -1)
1.274 + stream.close
1.275 + try_close()
1.276 +
1.277 + put_result(Kind.SYSTEM, "Message thread terminated")
1.278 }
1.279 }
1.280
1.281 @@ -363,16 +363,16 @@
1.282 /* isabelle version */
1.283
1.284 {
1.285 - val (msg, rc) = isabelle_system.isabelle_tool("version")
1.286 + val (msg, rc) = system.isabelle_tool("version")
1.287 if (rc != 0) error("Version check failed -- bad Isabelle installation:\n" + msg)
1.288 - put_result(Kind.SYSTEM, Nil, msg)
1.289 + put_result(Kind.SYSTEM, msg)
1.290 }
1.291
1.292
1.293 /* messages */
1.294
1.295 - val message_fifo = isabelle_system.mk_fifo()
1.296 - def rm_fifo() = isabelle_system.rm_fifo(message_fifo)
1.297 + val message_fifo = system.mk_fifo()
1.298 + def rm_fifo() = system.rm_fifo(message_fifo)
1.299
1.300 val message_thread = new MessageThread(message_fifo)
1.301 message_thread.start
1.302 @@ -381,9 +381,8 @@
1.303 /* exec process */
1.304
1.305 try {
1.306 - val cmdline =
1.307 - List(isabelle_system.getenv_strict("ISABELLE_PROCESS"), "-W", message_fifo) ++ args
1.308 - proc = isabelle_system.execute(true, cmdline: _*)
1.309 + val cmdline = List(system.getenv_strict("ISABELLE_PROCESS"), "-W", message_fifo) ++ args
1.310 + proc = system.execute(true, cmdline: _*)
1.311 }
1.312 catch {
1.313 case e: IOException =>
1.314 @@ -404,8 +403,8 @@
1.315 override def run() = {
1.316 val rc = proc.waitFor()
1.317 Thread.sleep(300)
1.318 - put_result(Kind.SYSTEM, Nil, "Exit thread terminated")
1.319 - put_result(Kind.EXIT, Nil, Integer.toString(rc))
1.320 + put_result(Kind.SYSTEM, "Exit thread terminated")
1.321 + put_result(Kind.EXIT, rc.toString)
1.322 rm_fifo()
1.323 }
1.324 }.start