limit build process output, to avoid bombing Isabelle/Scala process by ill-behaved jobs (e.g. Containers in AFP/9025435b29cf);

--- a/etc/options	Mon May 13 16:40:59 2013 +0200
+++ b/etc/options	Mon May 13 19:52:16 2013 +0200
@@ -81,6 +81,9 @@
 option timeout : real = 0
   -- "timeout for session build job (seconds > 0)"
 
+option process_output_limit : int = 100
+  -- "build process output limit in million characters (0 = unlimited)"
+
 
 section "Editor Reactivity"
 

--- a/src/Pure/System/isabelle_system.scala	Mon May 13 16:40:59 2013 +0200
+++ b/src/Pure/System/isabelle_system.scala	Mon May 13 19:52:16 2013 +0200
@@ -357,18 +357,33 @@
   }
 
   def bash_env(cwd: JFile, env: Map[String, String], script: String,
-    out_progress: String => Unit = (_: String) => (),
-    err_progress: String => Unit = (_: String) => ()): Bash_Result =
+    progress_stdout: String => Unit = (_: String) => (),
+    progress_stderr: String => Unit = (_: String) => (),
+    progress_limit: Option[Long] = None): 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
 
-      proc.stdin.close
+      val limited = new Object {
+        private var count = 0L
+        def apply(progress: String => Unit)(line: String): Unit = synchronized {
+          count = count + line.length + 1
+          progress_limit match {
+            case Some(limit) if count > limit => proc.terminate
+            case _ =>
+          }
+        }
+      }
       val (_, stdout) =
-        Simple_Thread.future("bash_stdout") { File.read_lines(proc.stdout, out_progress) }
+        Simple_Thread.future("bash_stdout") {
+          File.read_lines(proc.stdout, limited(progress_stdout))
+        }
       val (_, stderr) =
-        Simple_Thread.future("bash_stderr") { File.read_lines(proc.stderr, err_progress) }
+        Simple_Thread.future("bash_stderr") {
+          File.read_lines(proc.stderr, limited(progress_stderr))
+        }
 
       val rc =
         try { proc.join }

--- a/src/Pure/Tools/build.scala	Mon May 13 16:40:59 2013 +0200
+++ b/src/Pure/Tools/build.scala	Mon May 13 19:52:16 2013 +0200
@@ -526,10 +526,15 @@
     private val (thread, result) =
       Simple_Thread.future("build") {
         Isabelle_System.bash_env(info.dir.file, env, script,
-          out_progress = (line: String) =>
+          progress_stdout = (line: String) =>
             Library.try_unprefix("\floading_theory = ", line) match {
               case Some(theory) => progress.theory(name, theory)
               case None =>
+            },
+          progress_limit =
+            info.options.int("process_output_limit") match {
+              case 0 => None
+              case m => Some(m * 1000000L)
             })
       }