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

     2.1 --- a/src/Pure/System/isabelle_system.scala	Mon May 13 16:40:59 2013 +0200
     2.2 +++ b/src/Pure/System/isabelle_system.scala	Mon May 13 19:52:16 2013 +0200
     2.3 @@ -357,18 +357,33 @@
     2.4    }
     2.5  
     2.6    def bash_env(cwd: JFile, env: Map[String, String], script: String,
     2.7 -    out_progress: String => Unit = (_: String) => (),
     2.8 -    err_progress: String => Unit = (_: String) => ()): Bash_Result =
     2.9 +    progress_stdout: String => Unit = (_: String) => (),
    2.10 +    progress_stderr: String => Unit = (_: String) => (),
    2.11 +    progress_limit: Option[Long] = None): Bash_Result =
    2.12    {
    2.13      File.with_tmp_file("isabelle_script") { script_file =>
    2.14        File.write(script_file, script)
    2.15        val proc = new Managed_Process(cwd, env, false, "bash", posix_path(script_file))
    2.16 +      proc.stdin.close
    2.17  
    2.18 -      proc.stdin.close
    2.19 +      val limited = new Object {
    2.20 +        private var count = 0L
    2.21 +        def apply(progress: String => Unit)(line: String): Unit = synchronized {
    2.22 +          count = count + line.length + 1
    2.23 +          progress_limit match {
    2.24 +            case Some(limit) if count > limit => proc.terminate
    2.25 +            case _ =>
    2.26 +          }
    2.27 +        }
    2.28 +      }
    2.29        val (_, stdout) =
    2.30 -        Simple_Thread.future("bash_stdout") { File.read_lines(proc.stdout, out_progress) }
    2.31 +        Simple_Thread.future("bash_stdout") {
    2.32 +          File.read_lines(proc.stdout, limited(progress_stdout))
    2.33 +        }
    2.34        val (_, stderr) =
    2.35 -        Simple_Thread.future("bash_stderr") { File.read_lines(proc.stderr, err_progress) }
    2.36 +        Simple_Thread.future("bash_stderr") {
    2.37 +          File.read_lines(proc.stderr, limited(progress_stderr))
    2.38 +        }
    2.39  
    2.40        val rc =
    2.41          try { proc.join }

     3.1 --- a/src/Pure/Tools/build.scala	Mon May 13 16:40:59 2013 +0200
     3.2 +++ b/src/Pure/Tools/build.scala	Mon May 13 19:52:16 2013 +0200
     3.3 @@ -526,10 +526,15 @@
     3.4      private val (thread, result) =
     3.5        Simple_Thread.future("build") {
     3.6          Isabelle_System.bash_env(info.dir.file, env, script,
     3.7 -          out_progress = (line: String) =>
     3.8 +          progress_stdout = (line: String) =>
     3.9              Library.try_unprefix("\floading_theory = ", line) match {
    3.10                case Some(theory) => progress.theory(name, theory)
    3.11                case None =>
    3.12 +            },
    3.13 +          progress_limit =
    3.14 +            info.options.int("process_output_limit") match {
    3.15 +              case 0 => None
    3.16 +              case m => Some(m * 1000000L)
    3.17              })
    3.18        }
    3.19