# HG changeset patch
# User wenzelm
# Date 1596747498 -7200
# Node ID a1fb4d28e6090eb26b54bce0391e9152942503d7
# Parent  d9a42786fbc942579984fcc48f524c0b22fa68e9
unused --- superseded by PIDE messages;

diff -r d9a42786fbc9 -r a1fb4d28e609 src/Pure/System/bash.scala
--- a/src/Pure/System/bash.scala	Thu Aug 06 22:54:22 2020 +0200
+++ b/src/Pure/System/bash.scala	Thu Aug 06 22:58:18 2020 +0200
@@ -45,19 +45,6 @@
 
   /* process and result */
 
-  private class Limited_Progress(proc: Process, progress_limit: Option[Long])
-  {
-    private var count = 0L
-    def apply(progress: String => Unit)(line: String): Unit = synchronized {
-      progress(line)
-      count = count + line.length + 1
-      progress_limit match {
-        case Some(limit) if count > limit => proc.terminate
-        case _ =>
-      }
-    }
-  }
-
   def process(script: String,
       cwd: JFile = null,
       env: Map[String, String] = Isabelle_System.settings(),
@@ -181,16 +168,14 @@
     def result(
       progress_stdout: String => Unit = (_: String) => (),
       progress_stderr: String => Unit = (_: String) => (),
-      progress_limit: Option[Long] = None,
       strict: Boolean = true): Process_Result =
     {
       stdin.close
 
-      val limited = new Limited_Progress(this, progress_limit)
       val out_lines =
-        Future.thread("bash_stdout") { File.read_lines(stdout, limited(progress_stdout)) }
+        Future.thread("bash_stdout") { File.read_lines(stdout, progress_stdout) }
       val err_lines =
-        Future.thread("bash_stderr") { File.read_lines(stderr, limited(progress_stderr)) }
+        Future.thread("bash_stderr") { File.read_lines(stderr, progress_stderr) }
 
       val rc =
         try { join }
diff -r d9a42786fbc9 -r a1fb4d28e609 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Thu Aug 06 22:54:22 2020 +0200
+++ b/src/Pure/System/isabelle_system.scala	Thu Aug 06 22:58:18 2020 +0200
@@ -339,12 +339,11 @@
     redirect: Boolean = false,
     progress_stdout: String => Unit = (_: String) => (),
     progress_stderr: String => Unit = (_: String) => (),
-    progress_limit: Option[Long] = None,
     strict: Boolean = true,
     cleanup: () => Unit = () => ()): Process_Result =
   {
     Bash.process(script, cwd = cwd, env = env, redirect = redirect, cleanup = cleanup).
-      result(progress_stdout, progress_stderr, progress_limit, strict)
+      result(progress_stdout, progress_stderr, strict)
   }
 
   def jconsole(): Process_Result =