--- 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 */
--- 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)
--- 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)
}
}
--- 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)
- }
- }
}
//}}}
--- 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 =