src/Pure/Concurrent/bash.scala
changeset 62543 57f379ef662f
parent 62400 833af0d6d469
child 62545 8ebffdaf2ce2
equal deleted inserted replaced
62542:b27b7c2200b9 62543:57f379ef662f
    11   BufferedWriter, OutputStreamWriter}
    11   BufferedWriter, OutputStreamWriter}
    12 
    12 
    13 
    13 
    14 object Bash
    14 object Bash
    15 {
    15 {
       
    16   private class Limited_Progress(proc: Process, progress_limit: Option[Long])
       
    17   {
       
    18     private var count = 0L
       
    19     def apply(progress: String => Unit)(line: String): Unit = synchronized {
       
    20       progress(line)
       
    21       count = count + line.length + 1
       
    22       progress_limit match {
       
    23         case Some(limit) if count > limit => proc.terminate
       
    24         case _ =>
       
    25       }
       
    26     }
       
    27   }
       
    28 
    16   def process(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process =
    29   def process(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process =
    17     new Process(cwd, env, redirect, args:_*)
    30     new Process(cwd, env, redirect, args:_*)
    18 
    31 
    19   class Process private [Bash](
    32   class Process private [Bash](
    20       cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*)
    33       cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*)
    80     private def cleanup() =
    93     private def cleanup() =
    81       try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
    94       try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
    82       catch { case _: IllegalStateException => }
    95       catch { case _: IllegalStateException => }
    83 
    96 
    84 
    97 
       
    98     /* join */
       
    99 
       
   100     def join: Int = { val rc = proc.waitFor; cleanup(); rc }
       
   101 
       
   102 
    85     /* result */
   103     /* result */
    86 
   104 
    87     def join: Int = { val rc = proc.waitFor; cleanup(); rc }
   105     def result(
       
   106       progress_stdout: String => Unit = (_: String) => (),
       
   107       progress_stderr: String => Unit = (_: String) => (),
       
   108       progress_limit: Option[Long] = None,
       
   109       strict: Boolean = true): Process_Result =
       
   110     {
       
   111       stdin.close
       
   112 
       
   113       val limited = new Limited_Progress(this, progress_limit)
       
   114       val out_lines =
       
   115         Future.thread("bash_stdout") { File.read_lines(stdout, limited(progress_stdout)) }
       
   116       val err_lines =
       
   117         Future.thread("bash_stderr") { File.read_lines(stderr, limited(progress_stderr)) }
       
   118 
       
   119       val rc =
       
   120         try { join }
       
   121         catch { case Exn.Interrupt() => terminate; Exn.Interrupt.return_code }
       
   122       if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
       
   123 
       
   124       Process_Result(rc, out_lines.join, err_lines.join)
       
   125     }
    88   }
   126   }
    89 }
   127 }