clarified modules;
authorwenzelm
Wed Feb 24 22:11:28 2016 +0100 (2016-02-24)
changeset 62400833af0d6d469
parent 62399 36e885190439
child 62401 15a2533f1f0a
clarified modules;
src/Pure/Concurrent/bash.scala
src/Pure/System/isabelle_system.scala
src/Pure/System/process_result.scala
src/Pure/Tools/build.scala
src/Pure/build-jars
     1.1 --- a/src/Pure/Concurrent/bash.scala	Wed Feb 24 22:03:24 2016 +0100
     1.2 +++ b/src/Pure/Concurrent/bash.scala	Wed Feb 24 22:11:28 2016 +0100
     1.3 @@ -13,36 +13,6 @@
     1.4  
     1.5  object Bash
     1.6  {
     1.7 -  /** result **/
     1.8 -
     1.9 -  final case class Result(out_lines: List[String], err_lines: List[String], rc: Int)
    1.10 -  {
    1.11 -    def out: String = cat_lines(out_lines)
    1.12 -    def err: String = cat_lines(err_lines)
    1.13 -
    1.14 -    def error(s: String, err_rc: Int = 0): Result =
    1.15 -      copy(err_lines = err_lines ::: List(s), rc = rc max err_rc)
    1.16 -
    1.17 -    def ok: Boolean = rc == 0
    1.18 -    def interrupted: Boolean = rc == Exn.Interrupt.return_code
    1.19 -
    1.20 -    def check: Result =
    1.21 -      if (ok) this
    1.22 -      else if (interrupted) throw Exn.Interrupt()
    1.23 -      else Library.error(err)
    1.24 -
    1.25 -    def print: Result =
    1.26 -    {
    1.27 -      Output.warning(Library.trim_line(err))
    1.28 -      Output.writeln(Library.trim_line(out))
    1.29 -      Result(Nil, Nil, rc)
    1.30 -    }
    1.31 -  }
    1.32 -
    1.33 -
    1.34 -
    1.35 -  /** process **/
    1.36 -
    1.37    def process(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process =
    1.38      new Process(cwd, env, redirect, args:_*)
    1.39  
     2.1 --- a/src/Pure/System/isabelle_system.scala	Wed Feb 24 22:03:24 2016 +0100
     2.2 +++ b/src/Pure/System/isabelle_system.scala	Wed Feb 24 22:11:28 2016 +0100
     2.3 @@ -319,7 +319,7 @@
     2.4      progress_stdout: String => Unit = (_: String) => (),
     2.5      progress_stderr: String => Unit = (_: String) => (),
     2.6      progress_limit: Option[Long] = None,
     2.7 -    strict: Boolean = true): Bash.Result =
     2.8 +    strict: Boolean = true): Process_Result =
     2.9    {
    2.10      with_tmp_file("isabelle_script") { script_file =>
    2.11        File.write(script_file, script)
    2.12 @@ -337,7 +337,7 @@
    2.13          catch { case Exn.Interrupt() => proc.terminate; Exn.Interrupt.return_code }
    2.14        if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
    2.15  
    2.16 -      Bash.Result(stdout.join, stderr.join, rc)
    2.17 +      Process_Result(stdout.join, stderr.join, rc)
    2.18      }
    2.19    }
    2.20  
    2.21 @@ -367,10 +367,11 @@
    2.22    def pdf_viewer(arg: Path): Unit =
    2.23      bash("exec \"$PDF_VIEWER\" '" + File.standard_path(arg) + "' >/dev/null 2>/dev/null &")
    2.24  
    2.25 -  def hg(cmd_line: String, cwd: Path = Path.current): Bash.Result =
    2.26 +  def hg(cmd_line: String, cwd: Path = Path.current): Process_Result =
    2.27      bash("cd " + File.shell_path(cwd) + " && \"${HG:-hg}\" " + cmd_line)
    2.28  
    2.29  
    2.30 +
    2.31    /** Isabelle resources **/
    2.32  
    2.33    /* components */
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/System/process_result.scala	Wed Feb 24 22:11:28 2016 +0100
     3.3 @@ -0,0 +1,31 @@
     3.4 +/*  Title:      Pure/System/process_result.scala
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +Result of system process.
     3.8 +*/
     3.9 +
    3.10 +package isabelle
    3.11 +
    3.12 +final case class Process_Result(out_lines: List[String], err_lines: List[String], rc: Int)
    3.13 +{
    3.14 +  def out: String = cat_lines(out_lines)
    3.15 +  def err: String = cat_lines(err_lines)
    3.16 +
    3.17 +  def error(s: String, err_rc: Int = 0): Process_Result =
    3.18 +    copy(err_lines = err_lines ::: List(s), rc = rc max err_rc)
    3.19 +
    3.20 +  def ok: Boolean = rc == 0
    3.21 +  def interrupted: Boolean = rc == Exn.Interrupt.return_code
    3.22 +
    3.23 +  def check: Process_Result =
    3.24 +    if (ok) this
    3.25 +    else if (interrupted) throw Exn.Interrupt()
    3.26 +    else Library.error(err)
    3.27 +
    3.28 +  def print: Process_Result =
    3.29 +  {
    3.30 +    Output.warning(Library.trim_line(err))
    3.31 +    Output.writeln(Library.trim_line(out))
    3.32 +    Process_Result(Nil, Nil, rc)
    3.33 +  }
    3.34 +}
     4.1 --- a/src/Pure/Tools/build.scala	Wed Feb 24 22:03:24 2016 +0100
     4.2 +++ b/src/Pure/Tools/build.scala	Wed Feb 24 22:11:28 2016 +0100
     4.3 @@ -628,7 +628,7 @@
     4.4        else None
     4.5      }
     4.6  
     4.7 -    def join: Bash.Result =
     4.8 +    def join: Process_Result =
     4.9      {
    4.10        val res = result.join
    4.11  
     5.1 --- a/src/Pure/build-jars	Wed Feb 24 22:03:24 2016 +0100
     5.2 +++ b/src/Pure/build-jars	Wed Feb 24 22:11:28 2016 +0100
     5.3 @@ -82,6 +82,7 @@
     5.4    System/options.scala
     5.5    System/platform.scala
     5.6    System/posix_interrupt.scala
     5.7 +  System/process_result.scala
     5.8    System/progress.scala
     5.9    System/system_channel.scala
    5.10    System/utf8.scala