--- a/src/Pure/Build/build_job.scala Mon Jul 01 12:37:03 2024 +0200
+++ b/src/Pure/Build/build_job.scala Mon Jul 01 12:40:54 2024 +0200
@@ -240,7 +240,7 @@
}
catch { case ERROR(err) => (Process_Result.RC.failure, List(err)) }
- session.protocol_command("Prover.stop", rc.toString)
+ session.protocol_command("Prover.stop", XML.Encode.int(rc))
Build_Session_Errors(errors)
true
}
@@ -360,17 +360,16 @@
Isabelle_Thread.interrupt_handler(_ => process.terminate()) {
Exn.capture { process.await_startup() } match {
case Exn.Res(_) =>
- val resources_yxml = resources.init_session_yxml
+ val resources_xml = resources.init_session_xml
val encode_options: XML.Encode.T[Options] =
options => session.prover_options(options).encode
- val args_yxml =
- YXML.string_of_body(
- {
- import XML.Encode._
- pair(string, list(pair(encode_options, list(pair(string, properties)))))(
- (session_name, info.theories))
- })
- session.protocol_command("build_session", resources_yxml, args_yxml)
+ val args_xml =
+ {
+ import XML.Encode._
+ pair(string, list(pair(encode_options, list(pair(string, properties)))))(
+ (session_name, info.theories))
+ }
+ session.protocol_command("build_session", resources_xml, args_xml)
Build_Session_Errors.result
case Exn.Exn(exn) => Exn.Res(List(Exn.message(exn)))
}