diff -r b3ca4a6ed74b -r 87ebf5a50283 src/Pure/Tools/build_job.scala --- a/src/Pure/Tools/build_job.scala Fri Apr 01 11:51:42 2022 +0200 +++ b/src/Pure/Tools/build_job.scala Fri Apr 01 17:06:10 2022 +0200 @@ -12,16 +12,15 @@ import scala.collection.mutable -object Build_Job -{ +object Build_Job { /* theory markup/messages from database */ def read_theory( db_context: Sessions.Database_Context, session_hierarchy: List[String], theory: String, - unicode_symbols: Boolean = false): Option[Command] = - { + unicode_symbols: Boolean = false + ): Option[Command] = { def read(name: String): Export.Entry = db_context.get_export(session_hierarchy, theory, name) @@ -40,8 +39,7 @@ yield i -> elem) val blobs = - blobs_files.map(file => - { + blobs_files.map(file => { val path = Path.explode(file) val name = Resources.file_node(path) val src_path = File.relative_path(node_name.master_dir_path, path).getOrElse(path) @@ -91,16 +89,14 @@ margin: Double = Pretty.default_margin, breakgain: Double = Pretty.default_breakgain, metric: Pretty.Metric = Symbol.Metric, - unicode_symbols: Boolean = false): Unit = - { + unicode_symbols: Boolean = false + ): Unit = { val store = Sessions.store(options) val session = new Session(options, Resources.empty) - using(store.open_database_context())(db_context => - { + using(store.open_database_context())(db_context => { val result = - db_context.input_database(session_name)((db, _) => - { + db_context.input_database(session_name)((db, _) => { val theories = store.read_theories(db, session_name) val errors = store.read_errors(db, session_name) store.read_build(db, session_name).map(info => (theories, errors, info.return_code)) @@ -154,8 +150,7 @@ /* Isabelle tool wrapper */ val isabelle_tool = Isabelle_Tool("log", "print messages from build database", - Scala_Project.here, args => - { + Scala_Project.here, args => { /* arguments */ var unicode_symbols = false @@ -207,8 +202,8 @@ log: Logger, session_setup: (String, Session) => Unit, val numa_node: Option[Int], - command_timings0: List[Properties.T]) -{ + command_timings0: List[Properties.T] +) { val options: Options = NUMA.policy_options(info.options, numa_node) private val sessions_structure = deps.sessions_structure @@ -240,8 +235,7 @@ new Session(options, resources) { override val cache: Term.Cache = store.cache - override def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info = - { + override def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info = { result_base.load_commands.get(name.expand) match { case Some(spans) => val syntax = result_base.theory_syntax(name) @@ -251,14 +245,12 @@ } } - object Build_Session_Errors - { + object Build_Session_Errors { private val promise: Promise[List[String]] = Future.promise def result: Exn.Result[List[String]] = promise.join_result def cancel(): Unit = promise.cancel() - def apply(errs: List[String]): Unit = - { + def apply(errs: List[String]): Unit = { try { promise.fulfill(errs) } catch { case _: IllegalStateException => } } @@ -279,8 +271,8 @@ def fun( name: String, acc: mutable.ListBuffer[Properties.T], - unapply: Properties.T => Option[Properties.T]): (String, Session.Protocol_Function) = - { + unapply: Properties.T => Option[Properties.T] + ): (String, Session.Protocol_Function) = { name -> ((msg: Prover.Protocol_Output) => unapply(msg.properties) match { case Some(props) => acc += props; true @@ -288,16 +280,13 @@ }) } - session.init_protocol_handler(new Session.Protocol_Handler - { + session.init_protocol_handler(new Session.Protocol_Handler { override def exit(): Unit = Build_Session_Errors.cancel() - private def build_session_finished(msg: Prover.Protocol_Output): Boolean = - { + private def build_session_finished(msg: Prover.Protocol_Output): Boolean = { val (rc, errors) = try { - val (rc, errs) = - { + val (rc, errs) = { import XML.Decode._ pair(int, list(x => x))(Symbol.decode_yxml(msg.text)) } @@ -341,81 +330,76 @@ fun(Markup.Task_Statistics.name, task_statistics, Markup.Task_Statistics.unapply)) }) - session.command_timings += Session.Consumer("command_timings") - { - case Session.Command_Timing(props) => - for { - elapsed <- Markup.Elapsed.unapply(props) - elapsed_time = Time.seconds(elapsed) - if elapsed_time.is_relevant && elapsed_time >= options.seconds("command_timing_threshold") - } command_timings += props.filter(Markup.command_timing_property) - } + session.command_timings += Session.Consumer("command_timings") { + case Session.Command_Timing(props) => + for { + elapsed <- Markup.Elapsed.unapply(props) + elapsed_time = Time.seconds(elapsed) + if elapsed_time.is_relevant && elapsed_time >= options.seconds("command_timing_threshold") + } command_timings += props.filter(Markup.command_timing_property) + } - session.runtime_statistics += Session.Consumer("ML_statistics") - { - case Session.Runtime_Statistics(props) => runtime_statistics += props - } + session.runtime_statistics += Session.Consumer("ML_statistics") { + case Session.Runtime_Statistics(props) => runtime_statistics += props + } - session.finished_theories += Session.Consumer[Document.Snapshot]("finished_theories") - { - case snapshot => - if (!progress.stopped) { - val rendering = new Rendering(snapshot, options, session) + session.finished_theories += Session.Consumer[Document.Snapshot]("finished_theories") { + case snapshot => + if (!progress.stopped) { + val rendering = new Rendering(snapshot, options, session) - def export_(name: String, xml: XML.Body, compress: Boolean = true): Unit = - { - if (!progress.stopped) { - val theory_name = snapshot.node_name.theory - val args = - Protocol.Export.Args(theory_name = theory_name, name = name, compress = compress) - val bytes = Bytes(Symbol.encode(YXML.string_of_body(xml))) - if (!bytes.is_empty) export_consumer(session_name, args, bytes) - } + def export_(name: String, xml: XML.Body, compress: Boolean = true): Unit = { + if (!progress.stopped) { + val theory_name = snapshot.node_name.theory + val args = + Protocol.Export.Args(theory_name = theory_name, name = name, compress = compress) + val bytes = Bytes(Symbol.encode(YXML.string_of_body(xml))) + if (!bytes.is_empty) export_consumer(session_name, args, bytes) } - def export_text(name: String, text: String, compress: Boolean = true): Unit = - export_(name, List(XML.Text(text)), compress = compress) + } + def export_text(name: String, text: String, compress: Boolean = true): Unit = + export_(name, List(XML.Text(text)), compress = compress) - for (command <- snapshot.snippet_command) { - export_text(Export.DOCUMENT_ID, command.id.toString, compress = false) - } + for (command <- snapshot.snippet_command) { + export_text(Export.DOCUMENT_ID, command.id.toString, compress = false) + } - export_text(Export.FILES, - cat_lines(snapshot.node_files.map(_.symbolic.node)), compress = false) + export_text(Export.FILES, + cat_lines(snapshot.node_files.map(_.symbolic.node)), compress = false) - for (((_, xml), i) <- snapshot.xml_markup_blobs().zipWithIndex) { - export_(Export.MARKUP + (i + 1), xml) - } - export_(Export.MARKUP, snapshot.xml_markup()) - export_(Export.MESSAGES, snapshot.messages.map(_._1)) + for (((_, xml), i) <- snapshot.xml_markup_blobs().zipWithIndex) { + export_(Export.MARKUP + (i + 1), xml) + } + export_(Export.MARKUP, snapshot.xml_markup()) + export_(Export.MESSAGES, snapshot.messages.map(_._1)) - val citations = Library.distinct(rendering.citations(Text.Range.full).map(_.info)) - export_text(Export.DOCUMENT_CITATIONS, cat_lines(citations)) - } - } + val citations = Library.distinct(rendering.citations(Text.Range.full).map(_.info)) + export_text(Export.DOCUMENT_CITATIONS, cat_lines(citations)) + } + } - session.all_messages += Session.Consumer[Any]("build_session_output") - { - case msg: Prover.Output => - val message = msg.message - if (msg.is_system) resources.log(Protocol.message_text(message)) + session.all_messages += Session.Consumer[Any]("build_session_output") { + case msg: Prover.Output => + val message = msg.message + if (msg.is_system) resources.log(Protocol.message_text(message)) - if (msg.is_stdout) { - stdout ++= Symbol.encode(XML.content(message)) - } - else if (msg.is_stderr) { - stderr ++= Symbol.encode(XML.content(message)) - } - else if (msg.is_exit) { - val err = - "Prover terminated" + - (msg.properties match { - case Markup.Process_Result(result) => ": " + result.print_rc - case _ => "" - }) - Build_Session_Errors(List(err)) - } - case _ => - } + if (msg.is_stdout) { + stdout ++= Symbol.encode(XML.content(message)) + } + else if (msg.is_stderr) { + stderr ++= Symbol.encode(XML.content(message)) + } + else if (msg.is_exit) { + val err = + "Prover terminated" + + (msg.properties match { + case Markup.Process_Result(result) => ": " + result.print_rc + case _ => "" + }) + Build_Session_Errors(List(err)) + } + case _ => + } session_setup(session_name, session) @@ -458,8 +442,7 @@ val (document_output, document_errors) = try { if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok && info.documents.nonEmpty) { - using(store.open_database_context())(db_context => - { + using(store.open_database_context())(db_context => { val documents = Document_Build.build_documents( Document_Build.context(session_name, deps, db_context, progress = progress), @@ -477,11 +460,9 @@ case Exn.Interrupt.ERROR(msg) => (Nil, List(msg)) } - val result = - { + val result = { val theory_timing = - theory_timings.iterator.map( - { case props @ Markup.Name(name) => name -> props }).toMap + theory_timings.iterator.map({ case props @ Markup.Name(name) => name -> props }).toMap val used_theory_timings = for { (name, _) <- deps(session_name).used_theories } yield theory_timing.getOrElse(name.theory, Markup.Name(name.theory)) @@ -520,14 +501,12 @@ def terminate(): Unit = future_result.cancel() def is_finished: Boolean = future_result.is_finished - private val timeout_request: Option[Event_Timer.Request] = - { + private val timeout_request: Option[Event_Timer.Request] = { if (info.timeout_ignored) None else Some(Event_Timer.request(Time.now() + info.timeout) { terminate() }) } - def join: (Process_Result, Option[String]) = - { + def join: (Process_Result, Option[String]) = { val result1 = future_result.join val was_timeout =