immediate theory progress for build_dialog;
more formal Bash_Result -- accumulate output as lines;

--- a/src/Pure/General/file.scala	Sat Jan 12 14:56:57 2013 +0100
+++ b/src/Pure/General/file.scala	Sat Jan 12 15:00:48 2013 +0100
@@ -75,6 +75,21 @@
   def read_gzip(path: Path): String = read_gzip(path.file)
 
 
+  /* read lines */
+
+  def read_lines(reader: BufferedReader, progress: String => Unit): List[String] =
+  {
+    val result = new mutable.ListBuffer[String]
+    var line: String = null
+    while ({ line = reader.readLine; line != null }) {
+      progress(line)
+      result += line
+    }
+    reader.close
+    result.toList
+  }
+
+
   /* try_read */
 
   def try_read(paths: Seq[Path]): String =

--- a/src/Pure/PIDE/markup.ML	Sat Jan 12 14:56:57 2013 +0100
+++ b/src/Pure/PIDE/markup.ML	Sat Jan 12 15:00:48 2013 +0100
@@ -133,6 +133,8 @@
   val invoke_scala: string -> string -> Properties.T
   val cancel_scala: string -> Properties.T
   val ML_statistics: Properties.entry
+  val loading_theory: string -> Properties.T
+  val dest_loading_theory: Properties.T -> string option
   val no_output: Output.output * Output.output
   val default_output: T -> Output.output * Output.output
   val add_mode: string -> (T -> Output.output * Output.output) -> unit
@@ -408,6 +410,11 @@
 
 val ML_statistics = (functionN, "ML_statistics");
 
+fun loading_theory name = [("function", "loading_theory"), ("name", name)];
+
+fun dest_loading_theory [("function", "loading_theory"), ("name", name)] = SOME name
+  | dest_loading_theory _ = NONE;
+
 
 
 (** print mode operations **)

--- a/src/Pure/System/isabelle_system.scala	Sat Jan 12 14:56:57 2013 +0100
+++ b/src/Pure/System/isabelle_system.scala	Sat Jan 12 15:00:48 2013 +0100
@@ -16,7 +16,6 @@
 
 import scala.io.Source
 import scala.util.matching.Regex
-import scala.collection.mutable
 
 
 object Isabelle_System
@@ -331,24 +330,35 @@
 
   /* bash */
 
-  def bash_env(cwd: JFile, env: Map[String, String], script: String): (String, String, Int) =
+  final case class Bash_Result(out_lines: List[String], err_lines: List[String], rc: Int)
+  {
+    def out: String = cat_lines(out_lines)
+    def err: String = cat_lines(err_lines)
+    def add_err(s: String): Bash_Result = copy(err_lines = err_lines ::: List(s))
+  }
+
+  def bash_env(cwd: JFile, env: Map[String, String], script: String,
+    out_progress: String => Unit = (_: String) => (),
+    err_progress: String => Unit = (_: String) => ()): Bash_Result =
   {
     File.with_tmp_file("isabelle_script") { script_file =>
       File.write(script_file, script)
       val proc = new Managed_Process(cwd, env, false, "bash", posix_path(script_file))
 
       proc.stdin.close
-      val (_, stdout) = Simple_Thread.future("bash_stdout") { File.read_stream(proc.stdout) }
-      val (_, stderr) = Simple_Thread.future("bash_stderr") { File.read_stream(proc.stderr) }
+      val (_, stdout) =
+        Simple_Thread.future("bash_stdout") { File.read_lines(proc.stdout, out_progress) }
+      val (_, stderr) =
+        Simple_Thread.future("bash_stderr") { File.read_lines(proc.stderr, err_progress) }
 
       val rc =
         try { proc.join }
         catch { case e: InterruptedException => Thread.interrupted; proc.terminate; 130 }
-      (stdout.join, stderr.join, rc)
+      Bash_Result(stdout.join, stderr.join, rc)
     }
   }
 
-  def bash(script: String): (String, String, Int) = bash_env(null, null, script)
+  def bash(script: String): Bash_Result = bash_env(null, null, script)
 
 
   /* system tools */

--- a/src/Pure/System/system_channel.scala	Sat Jan 12 14:56:57 2013 +0100
+++ b/src/Pure/System/system_channel.scala	Sat Jan 12 15:00:48 2013 +0100
@@ -45,8 +45,8 @@
       "FIFO=\"/tmp/isabelle-fifo-${PPID}-$$" + i + "\"\n" +
       "echo -n \"$FIFO\"\n" +
       "mkfifo -m 600 \"$FIFO\"\n"
-    val (out, err, rc) = Isabelle_System.bash(script)
-    if (rc == 0) out else error(err.trim)
+    val result = Isabelle_System.bash(script)
+    if (result.rc == 0) result.out else error(result.err)
   }
 
   private def rm_fifo(fifo: String): Boolean = (new JFile(fifo)).delete

--- a/src/Pure/Thy/thy_info.ML	Sat Jan 12 14:56:57 2013 +0100
+++ b/src/Pure/Thy/thy_info.ML	Sat Jan 12 15:00:48 2013 +0100
@@ -224,6 +224,7 @@
   let
     val _ = kill_thy name;
     val _ = Output.urgent_message ("Loading theory " ^ quote name ^ required_by " " initiators);
+    val _ = Output.protocol_message (Markup.loading_theory name) "" handle Fail _ => ();
 
     val {master = (thy_path, _), imports} = deps;
     val dir = Path.dir thy_path;

--- a/src/Pure/Tools/build.ML	Sat Jan 12 14:56:57 2013 +0100
+++ b/src/Pure/Tools/build.ML	Sat Jan 12 15:00:48 2013 +0100
@@ -22,7 +22,10 @@
 fun protocol_message props output =
   (case ML_statistics props output of
     SOME stats => writeln ("\fML_statistics = " ^ ML_Syntax.print_properties stats)
-  | NONE => raise Fail "Undefined Output.protocol_message");
+  | NONE =>
+      (case Markup.dest_loading_theory props of
+        SOME name => writeln ("\floading_theory = " ^ name)
+      | NONE => raise Fail "Undefined Output.protocol_message"));
 
 
 (* build *)

--- a/src/Pure/Tools/build.scala	Sat Jan 12 14:56:57 2013 +0100
+++ b/src/Pure/Tools/build.scala	Sat Jan 12 15:00:48 2013 +0100
@@ -22,6 +22,7 @@
   /** progress context **/
 
   class Progress {
+    def theory(name: String) {}
     def echo(msg: String) {}
     def stopped: Boolean = false
   }
@@ -412,7 +413,8 @@
 
   /* 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
@@ -479,7 +481,12 @@
       }
 
     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
@@ -494,17 +501,16 @@
       }
       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
     }
   }
 
@@ -516,6 +522,7 @@
   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)
 
@@ -634,22 +641,21 @@
           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
 
@@ -659,11 +665,11 @@
                 (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))
                 }
@@ -671,7 +677,7 @@
                 (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
@@ -709,7 +715,7 @@
                 }
                 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 {

--- a/src/Pure/Tools/build_dialog.scala	Sat Jan 12 14:56:57 2013 +0100
+++ b/src/Pure/Tools/build_dialog.scala	Sat Jan 12 15:00:48 2013 +0100
@@ -83,6 +83,7 @@
 
     val progress = new Build.Progress
     {
+      override def theory(name: String): Unit = echo("  theory " + name)
       override def echo(msg: String): Unit = Swing_Thread.now { text.append(msg + "\n") }
       override def stopped: Boolean =
         Swing_Thread.now { val b = is_stopped; is_stopped = false; b  }

--- a/src/Pure/library.scala	Sat Jan 12 14:56:57 2013 +0100
+++ b/src/Pure/library.scala	Sat Jan 12 15:00:48 2013 +0100
@@ -82,10 +82,6 @@
     else ""
   }
 
-  def trim_line(str: String): String =
-    if (str.endsWith("\n")) str.substring(0, str.length - 1)
-    else str
-
   def lowercase(str: String): String = str.toLowerCase(Locale.ENGLISH)
   def uppercase(str: String): String = str.toUpperCase(Locale.ENGLISH)