src/Pure/Tools/build_job.scala

 import java.util.HashMap
 
 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)
 
     def read_xml(name: String): XML.Body =
       YXML.parse_body(

           Command.Results.make(
             for (elem @ XML.Elem(Markup(_, Markup.Serial(i)), _) <- read_xml(Export.MESSAGES))
               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)
             Command.Blob(name, src_path, None)
           })

     verbose: Boolean = false,
     progress: Progress = new Progress,
     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))
         })
       result match {

 
 
   /* 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
     var theories: List[String] = Nil
     var margin = Pretty.default_margin

   store: Sessions.Store,
   do_store: Boolean,
   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
 
   private val future_result: Future[Process_Result] =

         new Resources(sessions_structure, base, log = log, command_timings = command_timings0)
       val session =
         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)
                 Command.build_blobs_info(syntax, name, spans)
               case None => Command.Blobs_Info.none
             }
           }
         }
 
-      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 => }
         }
       }
 

       val task_statistics = new mutable.ListBuffer[Properties.T]
 
       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
             case _ => false
           })
       }
 
-      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))
                 }
                 val errors =
                   for (err <- errs) yield {

               fun(Markup.Theory_Timing.name, theory_timings, Markup.Theory_Timing.unapply),
               fun(Markup.Session_Timing.name, session_timings, Markup.Session_Timing.unapply),
               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.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)
-
-              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)
-                }
+      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.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_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)
-              }
-
-              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))
-
-              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))
-
-            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 _ =>
-        }
+            }
+            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)
+            }
+
+            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))
+
+            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))
+
+          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)
 
       val eval_main = Command_Line.ML_tool("Isabelle_Process.init_build ()" :: eval_store)
 

         export_consumer.shutdown(close = true).map(Output.error_message_text)
 
       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),
                     output_sources = info.document_output,
                     output_pdf = info.document_output)

         catch {
           case exn: Document_Build.Build_Error => (exn.log_lines, List(exn.message))
           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))
 
         val more_output =

     }
 
   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 =
       timeout_request match {
         case None => false