# HG changeset patch # User wenzelm # Date 1384540270 -3600 # Node ID c39972ddd6723d3e09e47ec17587efdb49db5419 # Parent 3d37b2957a3ea80dbee796518c4ede0e2fe7c5dd more specific Protocol_Output: empty message.body, main content via bytes/text; diff -r 3d37b2957a3e -r c39972ddd672 src/Pure/General/bytes.scala --- a/src/Pure/General/bytes.scala Thu Nov 14 17:39:32 2013 +0100 +++ b/src/Pure/General/bytes.scala Fri Nov 15 19:31:10 2013 +0100 @@ -20,11 +20,19 @@ val str = s.toString if (str.isEmpty) empty else { - val bytes = str.getBytes(UTF8.charset) - new Bytes(bytes, 0, bytes.length) + val b = str.getBytes(UTF8.charset) + new Bytes(b, 0, b.length) } } + def apply(a: Array[Byte], offset: Int, length: Int): Bytes = + if (length == 0) empty + else { + val b = new Array[Byte](length) + java.lang.System.arraycopy(a, offset, b, 0, length) + new Bytes(b, 0, b.length) + } + /* read */ diff -r 3d37b2957a3e -r c39972ddd672 src/Pure/System/invoke_scala.scala --- a/src/Pure/System/invoke_scala.scala Thu Nov 14 17:39:32 2013 +0100 +++ b/src/Pure/System/invoke_scala.scala Fri Nov 15 19:31:10 2013 +0100 @@ -89,15 +89,14 @@ } private def invoke_scala( - prover: Session.Prover, output: Isabelle_Process.Output): Boolean = synchronized + prover: Session.Prover, msg: Isabelle_Process.Protocol_Output): Boolean = synchronized { - output.properties match { + msg.properties match { case Markup.Invoke_Scala(name, id) => futures += (id -> default_thread_pool.submit(() => { - val arg = XML.content(output.body) - val (tag, result) = Invoke_Scala.method(name, arg) + val (tag, result) = Invoke_Scala.method(name, msg.text) fulfill(prover, id, tag, result) })) true @@ -106,9 +105,9 @@ } private def cancel_scala( - prover: Session.Prover, output: Isabelle_Process.Output): Boolean = synchronized + prover: Session.Prover, msg: Isabelle_Process.Protocol_Output): Boolean = synchronized { - output.properties match { + msg.properties match { case Markup.Cancel_Scala(id) => futures.get(id) match { case Some(future) => cancel(prover, id, future) diff -r 3d37b2957a3e -r c39972ddd672 src/Pure/System/isabelle_process.scala --- a/src/Pure/System/isabelle_process.scala Thu Nov 14 17:39:32 2013 +0100 +++ b/src/Pure/System/isabelle_process.scala Fri Nov 15 19:31:10 2013 +0100 @@ -49,8 +49,7 @@ override def toString: String = { val res = - if (is_status || is_report) message.body.map(_.toString).mkString - else if (is_protocol) "..." + if (is_status || is_report || is_protocol) message.body.map(_.toString).mkString else Pretty.string_of(message.body) if (properties.isEmpty) kind.toString + " [[" + res + "]]" @@ -59,6 +58,12 @@ (for ((x, y) <- properties) yield x + "=" + y).mkString("{", ",", "}") + " [[" + res + "]]" } } + + class Protocol_Output(props: Properties.T, val bytes: Bytes) + extends Output(XML.Elem(Markup(Markup.PROTOCOL, props), Nil)) + { + lazy val text: String = bytes.toString + } } @@ -89,22 +94,23 @@ receiver(new Output(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text))))) } - private def output_message(kind: String, props: Properties.T, body: XML.Body) + private def protocol_output(props: Properties.T, bytes: Bytes) + { + receiver(new Protocol_Output(props, bytes)) + } + + private def output(kind: String, props: Properties.T, body: XML.Body) { if (kind == Markup.INIT) system_channel.accepted() - if (kind == Markup.PROTOCOL) - receiver(new Output(XML.Elem(Markup(kind, props), body))) - else { - val main = XML.Elem(Markup(kind, props), Protocol.clean_message(body)) - val reports = Protocol.message_reports(props, body) - for (msg <- main :: reports) receiver(new Output(xml_cache.elem(msg))) - } + + val main = XML.Elem(Markup(kind, props), Protocol.clean_message(body)) + val reports = Protocol.message_reports(props, body) + for (msg <- main :: reports) receiver(new Output(xml_cache.elem(msg))) } private def exit_message(rc: Int) { - output_message(Markup.EXIT, Markup.Return_Code(rc), - List(XML.Text("Return code: " + rc.toString))) + output(Markup.EXIT, Markup.Return_Code(rc), List(XML.Text("Return code: " + rc.toString))) } @@ -232,7 +238,7 @@ else done = true } if (result.length > 0) { - output_message(markup, Nil, List(XML.Text(decode(result.toString)))) + output(markup, Nil, List(XML.Text(decode(result.toString)))) result.length = 0 } else { @@ -306,7 +312,7 @@ } //}}} - def read_chunk(do_decode: Boolean): XML.Body = + def read_chunk_bytes(): (Array[Byte], Int) = //{{{ { val n = read_int() @@ -325,23 +331,33 @@ if (i != n) throw new Protocol_Error("bad chunk (unexpected EOF after " + i + " of " + n + " bytes)") - if (do_decode) - YXML.parse_body_failsafe(UTF8.decode_chars(decode, buf, 0, n)) - else List(XML.Text(UTF8.decode_chars(s => s, buf, 0, n).toString)) + (buf, n) } //}}} + def read_chunk(): XML.Body = + { + val (buf, n) = read_chunk_bytes() + YXML.parse_body_failsafe(UTF8.decode_chars(decode, buf, 0, n)) + } + try { do { try { - val header = read_chunk(true) + val header = read_chunk() header match { case List(XML.Elem(Markup(name, props), Nil)) => val kind = name.intern - val body = read_chunk(kind != Markup.PROTOCOL) - output_message(kind, props, body) + if (kind == Markup.PROTOCOL) { + val (buf, n) = read_chunk_bytes() + protocol_output(props, Bytes(buf, 0, n)) + } + else { + val body = read_chunk() + output(kind, props, body) + } case _ => - read_chunk(false) + read_chunk() throw new Protocol_Error("bad header: " + header.toString) } } diff -r 3d37b2957a3e -r c39972ddd672 src/Pure/System/session.scala --- a/src/Pure/System/session.scala Thu Nov 14 17:39:32 2013 +0100 +++ b/src/Pure/System/session.scala Fri Nov 15 19:31:10 2013 +0100 @@ -46,12 +46,12 @@ abstract class Protocol_Handler { def stop(prover: Prover): Unit = {} - val functions: Map[String, (Prover, Isabelle_Process.Output) => Boolean] + val functions: Map[String, (Prover, Isabelle_Process.Protocol_Output) => Boolean] } class Protocol_Handlers( handlers: Map[String, Session.Protocol_Handler] = Map.empty, - functions: Map[String, Isabelle_Process.Output => Boolean] = Map.empty) + functions: Map[String, Isabelle_Process.Protocol_Output => Boolean] = Map.empty) { def get(name: String): Option[Protocol_Handler] = handlers.get(name) @@ -71,7 +71,7 @@ val new_handler = Class.forName(name).newInstance.asInstanceOf[Protocol_Handler] val new_functions = for ((a, f) <- new_handler.functions.toList) yield - (a, (output: Isabelle_Process.Output) => f(prover, output)) + (a, (msg: Isabelle_Process.Protocol_Output) => f(prover, msg)) val dups = for ((a, _) <- new_functions if functions1.isDefinedAt(a)) yield a if (!dups.isEmpty) error("Duplicate protocol functions: " + commas_quote(dups)) @@ -88,10 +88,10 @@ new Protocol_Handlers(handlers2, functions2) } - def invoke(output: Isabelle_Process.Output): Boolean = - output.properties match { + def invoke(msg: Isabelle_Process.Protocol_Output): Boolean = + msg.properties match { case Markup.Function(a) if functions.isDefinedAt(a) => - try { functions(a)(output) } + try { functions(a)(msg) } catch { case exn: Throwable => System.err.println("Failed invocation of protocol function: " + @@ -414,69 +414,69 @@ } } - if (output.is_protocol) { - val handled = _protocol_handlers.invoke(output) - if (!handled) { - output.properties match { - case Markup.Protocol_Handler(name) => - _protocol_handlers = _protocol_handlers.add(prover.get, name) + output match { + case msg: Isabelle_Process.Protocol_Output => + val handled = _protocol_handlers.invoke(msg) + if (!handled) { + msg.properties match { + case Markup.Protocol_Handler(name) => + _protocol_handlers = _protocol_handlers.add(prover.get, name) + + case Protocol.Command_Timing(state_id, timing) => + val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil))) + accumulate(state_id, prover.get.xml_cache.elem(message)) - case Protocol.Command_Timing(state_id, timing) => - val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil))) - accumulate(state_id, prover.get.xml_cache.elem(message)) + case Markup.Assign_Update => + msg.text match { + case Protocol.Assign_Update(id, update) => + try { + val cmds = global_state >>> (_.assign(id, update)) + delay_commands_changed.invoke(true, cmds) + } + catch { case _: Document.State.Fail => bad_output() } + case _ => bad_output() + } + // FIXME separate timeout event/message!? + if (prover.isDefined && System.currentTimeMillis() > prune_next) { + val old_versions = global_state >>> (_.prune_history(prune_size)) + if (!old_versions.isEmpty) prover.get.remove_versions(old_versions) + prune_next = System.currentTimeMillis() + prune_delay.ms + } - case Markup.Assign_Update => - XML.content(output.body) match { - case Protocol.Assign_Update(id, update) => - try { - val cmds = global_state >>> (_.assign(id, update)) - delay_commands_changed.invoke(true, cmds) - } - catch { case _: Document.State.Fail => bad_output() } - case _ => bad_output() - } - // FIXME separate timeout event/message!? - if (prover.isDefined && System.currentTimeMillis() > prune_next) { - val old_versions = global_state >>> (_.prune_history(prune_size)) - if (!old_versions.isEmpty) prover.get.remove_versions(old_versions) - prune_next = System.currentTimeMillis() + prune_delay.ms - } + case Markup.Removed_Versions => + msg.text match { + case Protocol.Removed(removed) => + try { + global_state >> (_.removed_versions(removed)) + } + catch { case _: Document.State.Fail => bad_output() } + case _ => bad_output() + } + + case Markup.ML_Statistics(props) => + statistics.event(Session.Statistics(props)) + + case Markup.Task_Statistics(props) => + // FIXME - case Markup.Removed_Versions => - XML.content(output.body) match { - case Protocol.Removed(removed) => - try { - global_state >> (_.removed_versions(removed)) - } - catch { case _: Document.State.Fail => bad_output() } - case _ => bad_output() - } - - case Markup.ML_Statistics(props) => - statistics.event(Session.Statistics(props)) - - case Markup.Task_Statistics(props) => - // FIXME - - case _ => bad_output() + case _ => bad_output() + } + } + case _ => + output.properties match { + case Position.Id(state_id) => + accumulate(state_id, output.message) + + case _ if output.is_init => + phase = Session.Ready + + case Markup.Return_Code(rc) if output.is_exit => + if (rc == 0) phase = Session.Inactive + else phase = Session.Failed + + case _ => raw_output_messages.event(output) } } - } - else { - output.properties match { - case Position.Id(state_id) => - accumulate(state_id, output.message) - - case _ if output.is_init => - phase = Session.Ready - - case Markup.Return_Code(rc) if output.is_exit => - if (rc == 0) phase = Session.Inactive - else phase = Session.Failed - - case _ => raw_output_messages.event(output) - } - } } //}}} diff -r 3d37b2957a3e -r c39972ddd672 src/Pure/Tools/sledgehammer_params.scala --- a/src/Pure/Tools/sledgehammer_params.scala Thu Nov 14 17:39:32 2013 +0100 +++ b/src/Pure/Tools/sledgehammer_params.scala Fri Nov 15 19:31:10 2013 +0100 @@ -37,13 +37,10 @@ def get_provers: String = synchronized { _provers } private def sledgehammer_provers( - prover: Session.Prover, output: Isabelle_Process.Output): Boolean = + prover: Session.Prover, msg: Isabelle_Process.Protocol_Output): Boolean = { - output.body match { - case Nil => update_provers(""); true - case List(XML.Text(s)) => update_provers(s); true - case _ => false - } + update_provers(msg.text) + true } val functions =