clarified modules, like ML version;
authorwenzelm
Thu Aug 20 20:36:06 2015 +0200 (2015-08-20)
changeset 609912fc5a44346b5
parent 60990 07592e217180
child 60992 89effcb342df
clarified modules, like ML version;
src/Pure/Concurrent/bash.scala
src/Pure/System/isabelle_process.scala
src/Pure/System/isabelle_system.scala
src/Pure/Tools/build.scala
src/Pure/build-jars
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Concurrent/bash.scala	Thu Aug 20 20:36:06 2015 +0200
     1.3 @@ -0,0 +1,106 @@
     1.4 +/*  Title:      Pure/Concurrent/bash.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +GNU bash processes, with propagation of interrupts.
     1.8 +*/
     1.9 +
    1.10 +package isabelle
    1.11 +
    1.12 +
    1.13 +import java.io.{File => JFile, BufferedReader, InputStreamReader,
    1.14 +  BufferedWriter, OutputStreamWriter}
    1.15 +
    1.16 +
    1.17 +object Bash
    1.18 +{
    1.19 +  /** result **/
    1.20 +
    1.21 +  final case class Result(out_lines: List[String], err_lines: List[String], rc: Int)
    1.22 +  {
    1.23 +    def out: String = cat_lines(out_lines)
    1.24 +    def err: String = cat_lines(err_lines)
    1.25 +    def add_err(s: String): Result = copy(err_lines = err_lines ::: List(s))
    1.26 +    def set_rc(i: Int): Result = copy(rc = i)
    1.27 +
    1.28 +    def check_error: Result =
    1.29 +      if (rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
    1.30 +      else if (rc != 0) error(err)
    1.31 +      else this
    1.32 +  }
    1.33 +
    1.34 +
    1.35 +
    1.36 +  /** process **/
    1.37 +
    1.38 +  def process(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process =
    1.39 +    new Process(cwd, env, redirect, args:_*)
    1.40 +
    1.41 +  class Process private [Bash](
    1.42 +      cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*)
    1.43 +    extends Prover.System_Process
    1.44 +  {
    1.45 +    private val params =
    1.46 +      List(File.standard_path(Path.explode("~~/lib/scripts/process")), "group", "-", "no_script")
    1.47 +    private val proc = Isabelle_System.execute_env(cwd, env, redirect, (params ::: args.toList):_*)
    1.48 +
    1.49 +
    1.50 +    // channels
    1.51 +
    1.52 +    val stdin: BufferedWriter =
    1.53 +      new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, UTF8.charset))
    1.54 +
    1.55 +    val stdout: BufferedReader =
    1.56 +      new BufferedReader(new InputStreamReader(proc.getInputStream, UTF8.charset))
    1.57 +
    1.58 +    val stderr: BufferedReader =
    1.59 +      new BufferedReader(new InputStreamReader(proc.getErrorStream, UTF8.charset))
    1.60 +
    1.61 +
    1.62 +    // signals
    1.63 +
    1.64 +    private val pid = stdout.readLine
    1.65 +
    1.66 +    private def kill_cmd(signal: String): Int =
    1.67 +      Isabelle_System.execute(true, "/usr/bin/env", "bash", "-c", "kill -" + signal + " -" + pid)
    1.68 +        .waitFor
    1.69 +
    1.70 +    private def kill(signal: String): Boolean =
    1.71 +      Exn.Interrupt.postpone { kill_cmd(signal); kill_cmd("0") == 0 } getOrElse true
    1.72 +
    1.73 +    private def multi_kill(signal: String): Boolean =
    1.74 +    {
    1.75 +      var running = true
    1.76 +      var count = 10
    1.77 +      while (running && count > 0) {
    1.78 +        if (kill(signal)) {
    1.79 +          Exn.Interrupt.postpone {
    1.80 +            Thread.sleep(100)
    1.81 +            count -= 1
    1.82 +          }
    1.83 +        }
    1.84 +        else running = false
    1.85 +      }
    1.86 +      running
    1.87 +    }
    1.88 +
    1.89 +    def interrupt() { multi_kill("INT") }
    1.90 +    def terminate() { multi_kill("INT") && multi_kill("TERM") && kill("KILL"); proc.destroy }
    1.91 +
    1.92 +
    1.93 +    // JVM shutdown hook
    1.94 +
    1.95 +    private val shutdown_hook = new Thread { override def run = terminate() }
    1.96 +
    1.97 +    try { Runtime.getRuntime.addShutdownHook(shutdown_hook) }
    1.98 +    catch { case _: IllegalStateException => }
    1.99 +
   1.100 +    private def cleanup() =
   1.101 +      try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
   1.102 +      catch { case _: IllegalStateException => }
   1.103 +
   1.104 +
   1.105 +    /* result */
   1.106 +
   1.107 +    def join: Int = { val rc = proc.waitFor; cleanup(); rc }
   1.108 +  }
   1.109 +}
     2.1 --- a/src/Pure/System/isabelle_process.scala	Thu Aug 20 19:33:26 2015 +0200
     2.2 +++ b/src/Pure/System/isabelle_process.scala	Thu Aug 20 20:36:06 2015 +0200
     2.3 @@ -19,9 +19,7 @@
     2.4          val cmdline =
     2.5            Isabelle_System.getenv_strict("ISABELLE_PROCESS") ::
     2.6              (system_channel.prover_args ::: prover_args)
     2.7 -        val process =
     2.8 -          new Isabelle_System.Managed_Process(null, null, false, cmdline: _*) with
     2.9 -            Prover.System_Process
    2.10 +        val process = Bash.process(null, null, false, cmdline: _*)
    2.11          process.stdin.close
    2.12          process
    2.13        }
     3.1 --- a/src/Pure/System/isabelle_system.scala	Thu Aug 20 19:33:26 2015 +0200
     3.2 +++ b/src/Pure/System/isabelle_system.scala	Thu Aug 20 20:36:06 2015 +0200
     3.3 @@ -9,8 +9,7 @@
     3.4  
     3.5  
     3.6  import java.util.regex.Pattern
     3.7 -import java.io.{File => JFile, BufferedReader, InputStreamReader,
     3.8 -  BufferedWriter, OutputStreamWriter, IOException}
     3.9 +import java.io.{File => JFile, IOException}
    3.10  import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult}
    3.11  import java.nio.file.attribute.BasicFileAttributes
    3.12  import java.net.{URL, URLDecoder, MalformedURLException}
    3.13 @@ -294,75 +293,6 @@
    3.14      execute_env(null, null, redirect, args: _*)
    3.15  
    3.16  
    3.17 -  /* managed process */
    3.18 -
    3.19 -  class Managed_Process(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*)
    3.20 -  {
    3.21 -    private val params =
    3.22 -      List(File.standard_path(Path.explode("~~/lib/scripts/process")), "group", "-", "no_script")
    3.23 -    private val proc = execute_env(cwd, env, redirect, (params ::: args.toList):_*)
    3.24 -
    3.25 -
    3.26 -    // channels
    3.27 -
    3.28 -    val stdin: BufferedWriter =
    3.29 -      new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, UTF8.charset))
    3.30 -
    3.31 -    val stdout: BufferedReader =
    3.32 -      new BufferedReader(new InputStreamReader(proc.getInputStream, UTF8.charset))
    3.33 -
    3.34 -    val stderr: BufferedReader =
    3.35 -      new BufferedReader(new InputStreamReader(proc.getErrorStream, UTF8.charset))
    3.36 -
    3.37 -
    3.38 -    // signals
    3.39 -
    3.40 -    private val pid = stdout.readLine
    3.41 -
    3.42 -    private def kill_cmd(signal: String): Int =
    3.43 -      execute(true, "/usr/bin/env", "bash", "-c", "kill -" + signal + " -" + pid).waitFor
    3.44 -
    3.45 -    private def kill(signal: String): Boolean =
    3.46 -      Exn.Interrupt.postpone { kill_cmd(signal); kill_cmd("0") == 0 } getOrElse true
    3.47 -
    3.48 -    private def multi_kill(signal: String): Boolean =
    3.49 -    {
    3.50 -      var running = true
    3.51 -      var count = 10
    3.52 -      while (running && count > 0) {
    3.53 -        if (kill(signal)) {
    3.54 -          Exn.Interrupt.postpone {
    3.55 -            Thread.sleep(100)
    3.56 -            count -= 1
    3.57 -          }
    3.58 -        }
    3.59 -        else running = false
    3.60 -      }
    3.61 -      running
    3.62 -    }
    3.63 -
    3.64 -    def interrupt() { multi_kill("INT") }
    3.65 -    def terminate() { multi_kill("INT") && multi_kill("TERM") && kill("KILL"); proc.destroy }
    3.66 -
    3.67 -
    3.68 -    // JVM shutdown hook
    3.69 -
    3.70 -    private val shutdown_hook = new Thread { override def run = terminate() }
    3.71 -
    3.72 -    try { Runtime.getRuntime.addShutdownHook(shutdown_hook) }
    3.73 -    catch { case _: IllegalStateException => }
    3.74 -
    3.75 -    private def cleanup() =
    3.76 -      try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
    3.77 -      catch { case _: IllegalStateException => }
    3.78 -
    3.79 -
    3.80 -    /* result */
    3.81 -
    3.82 -    def join: Int = { val rc = proc.waitFor; cleanup(); rc }
    3.83 -  }
    3.84 -
    3.85 -
    3.86    /* tmp files */
    3.87  
    3.88    private def isabelle_tmp_prefix(): JFile =
    3.89 @@ -430,20 +360,7 @@
    3.90  
    3.91    /* bash */
    3.92  
    3.93 -  final case class Bash_Result(out_lines: List[String], err_lines: List[String], rc: Int)
    3.94 -  {
    3.95 -    def out: String = cat_lines(out_lines)
    3.96 -    def err: String = cat_lines(err_lines)
    3.97 -    def add_err(s: String): Bash_Result = copy(err_lines = err_lines ::: List(s))
    3.98 -    def set_rc(i: Int): Bash_Result = copy(rc = i)
    3.99 -
   3.100 -    def check_error: Bash_Result =
   3.101 -      if (rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
   3.102 -      else if (rc != 0) error(err)
   3.103 -      else this
   3.104 -  }
   3.105 -
   3.106 -  private class Limited_Progress(proc: Managed_Process, progress_limit: Option[Long])
   3.107 +  private class Limited_Progress(proc: Bash.Process, progress_limit: Option[Long])
   3.108    {
   3.109      private var count = 0L
   3.110      def apply(progress: String => Unit)(line: String): Unit = synchronized {
   3.111 @@ -460,11 +377,11 @@
   3.112      progress_stdout: String => Unit = (_: String) => (),
   3.113      progress_stderr: String => Unit = (_: String) => (),
   3.114      progress_limit: Option[Long] = None,
   3.115 -    strict: Boolean = true): Bash_Result =
   3.116 +    strict: Boolean = true): Bash.Result =
   3.117    {
   3.118      with_tmp_file("isabelle_script") { script_file =>
   3.119        File.write(script_file, script)
   3.120 -      val proc = new Managed_Process(cwd, env, false, "bash", posix_path(script_file))
   3.121 +      val proc = Bash.process(cwd, env, false, "bash", posix_path(script_file))
   3.122        proc.stdin.close
   3.123  
   3.124        val limited = new Limited_Progress(proc, progress_limit)
   3.125 @@ -482,11 +399,11 @@
   3.126          catch { case Exn.Interrupt() => proc.terminate; Exn.Interrupt.return_code }
   3.127        if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
   3.128  
   3.129 -      Bash_Result(stdout.join, stderr.join, rc)
   3.130 +      Bash.Result(stdout.join, stderr.join, rc)
   3.131      }
   3.132    }
   3.133  
   3.134 -  def bash(script: String): Bash_Result = bash_env(null, null, script)
   3.135 +  def bash(script: String): Bash.Result = bash_env(null, null, script)
   3.136  
   3.137  
   3.138    /* system tools */
   3.139 @@ -514,7 +431,7 @@
   3.140    def pdf_viewer(arg: Path): Unit =
   3.141      bash("exec \"$PDF_VIEWER\" '" + File.standard_path(arg) + "' >/dev/null 2>/dev/null &")
   3.142  
   3.143 -  def hg(cmd_line: String, cwd: Path = Path.current): Bash_Result =
   3.144 +  def hg(cmd_line: String, cwd: Path = Path.current): Bash.Result =
   3.145      bash("cd " + File.shell_path(cwd) + " && \"${HG:-hg}\" " + cmd_line)
   3.146  
   3.147  
     4.1 --- a/src/Pure/Tools/build.scala	Thu Aug 20 19:33:26 2015 +0200
     4.2 +++ b/src/Pure/Tools/build.scala	Thu Aug 20 20:36:06 2015 +0200
     4.3 @@ -653,7 +653,7 @@
     4.4        else None
     4.5      }
     4.6  
     4.7 -    def join: Isabelle_System.Bash_Result =
     4.8 +    def join: Bash.Result =
     4.9      {
    4.10        val res = result.join
    4.11  
     5.1 --- a/src/Pure/build-jars	Thu Aug 20 19:33:26 2015 +0200
     5.2 +++ b/src/Pure/build-jars	Thu Aug 20 20:36:06 2015 +0200
     5.3 @@ -9,6 +9,7 @@
     5.4  ## sources
     5.5  
     5.6  declare -a SOURCES=(
     5.7 +  Concurrent/bash.scala
     5.8    Concurrent/consumer_thread.scala
     5.9    Concurrent/counter.scala
    5.10    Concurrent/event_timer.scala