src/Pure/Tools/build.scala

 object Build
 {
   /** progress context **/
 
   class Progress {
+    def theory(name: String) {}
     def echo(msg: String) {}
     def stopped: Boolean = false
   }
 
   object Ignore_Progress extends Progress

     session_content(false, Nil, session).check_errors.syntax
 
 
   /* jobs */
 
-  private class Job(name: String, val info: Session_Info, output: Path, do_output: Boolean,
+  private class Job(progress: Build.Progress,
+    name: String, val info: Session_Info, output: Path, do_output: Boolean,
     verbose: Boolean, browser_info: Path)
   {
     // global browser info dir
     if (info.options.bool("browser_info") && !(browser_info + Path.explode("index.html")).is_file)
     {

         exit "$RC"
         """
       }
 
     private val (thread, result) =
-      Simple_Thread.future("build") { Isabelle_System.bash_env(info.dir.file, env, script) }
+      Simple_Thread.future("build") {
+        Isabelle_System.bash_env(info.dir.file, env, script,
+          out_progress = (line: String) =>
+            if (line.startsWith(LOADING_THEORY))
+              progress.theory(line.substring(LOADING_THEORY.length)))
+      }
 
     def terminate: Unit = thread.interrupt
     def is_finished: Boolean = result.is_finished
 
     @volatile private var timeout = false

         t.schedule(new TimerTask { def run = { terminate; timeout = true } }, time.ms)
         Some(t)
       }
       else None
 
-    def join: (String, String, Int) = {
-      val (out, err, rc) = result.join
+    def join: Isabelle_System.Bash_Result =
+    {
+      val res = result.join
+
       args_file.delete
       timer.map(_.cancel())
 
-      val err1 =
-        if (rc == 130)
-          (if (err.isEmpty || err.endsWith("\n")) err else err + "\n") +
-          (if (timeout) "*** Timeout\n" else "*** Interrupt\n")
-        else err
-      (out, err1, rc)
+      if (res.rc == 130)
+        res.add_err(if (timeout) "*** Timeout" else "*** Interrupt")
+      else res
     }
   }
 
 
   /* log files */

   private val LOG = Path.explode("log")
   private def log(name: String): Path = LOG + Path.basic(name)
   private def log_gz(name: String): Path = log(name).ext("gz")
 
   private val SESSION_PARENT_PATH = "\fSession.parent_path = "
+  private val LOADING_THEORY = "\floading_theory = "
 
   sealed case class Log_Info(stats: List[Properties.T], timing: Properties.T)
 
   def parse_log(text: String): Log_Info =
   {

       else
         running.find({ case (_, (_, job)) => job.is_finished }) match {
           case Some((name, (parent_heap, job))) =>
             //{{{ finish job
 
-            val (out, err, rc) = job.join
-            val out_lines = split_lines(out)
-            progress.echo(Library.trim_line(err))
+            val res = job.join
+            progress.echo(res.err)
 
             val (parent_path, heap) =
-              if (rc == 0) {
+              if (res.rc == 0) {
                 (output_dir + log(name)).file.delete
 
                 val sources = make_stamp(name)
                 val heap = heap_stamp(job.output_path)
                 File.write_gzip(output_dir + log_gz(name),
-                  sources + "\n" + parent_heap + "\n" + heap + "\n" + out)
+                  sources + "\n" + parent_heap + "\n" + heap + "\n" + res.out)
 
                 val parent_path =
                   if (job.info.options.bool("browser_info"))
-                    out_lines.find(_.startsWith(SESSION_PARENT_PATH)).map(line =>
+                    res.out_lines.find(_.startsWith(SESSION_PARENT_PATH)).map(line =>
                       line.substring(SESSION_PARENT_PATH.length))
                   else None
 
                 (parent_path, heap)
               }
               else {
                 (output_dir + Path.basic(name)).file.delete
                 (output_dir + log_gz(name)).file.delete
 
-                File.write(output_dir + log(name), out)
+                File.write(output_dir + log(name), res.out)
                 progress.echo(name + " FAILED")
-                if (rc != 130) {
+                if (res.rc != 130) {
                   progress.echo("(see also " + (output_dir + log(name)).file.toString + ")")
-                  val lines = out_lines.filterNot(_.startsWith("\f"))
+                  val lines = res.out_lines.filterNot(_.startsWith("\f"))
                   val tail = lines.drop(lines.length - 20 max 0)
                   progress.echo("\n" + cat_lines(tail))
                 }
 
                 (None, no_heap)
               }
             loop(pending - name, running - name,
-              results + (name -> Result(false, parent_path, heap, rc)))
+              results + (name -> Result(false, parent_path, heap, res.rc)))
             //}}}
           case None if (running.size < (max_jobs max 1)) =>
             //{{{ check/start next job
             pending.dequeue(running.isDefinedAt(_)) match {
               case Some((name, info)) =>

                   if (verbose) progress.echo("Skipping " + name + " ...")
                   loop(pending - name, running, results + (name -> Result(false, None, heap, 1)))
                 }
                 else if (parent_result.rc == 0) {
                   progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
-                  val job = new Job(name, info, output, do_output, verbose, browser_info)
+                  val job = new Job(progress, name, info, output, do_output, verbose, browser_info)
                   loop(pending, running + (name -> (parent_result.heap, job)), results)
                 }
                 else {
                   progress.echo(name + " CANCELLED")
                   loop(pending - name, running, results + (name -> Result(false, None, heap, 1)))