# HG changeset patch # User wenzelm # Date 1456348288 -3600 # Node ID 833af0d6d4695620e74f689457249cd479a07223 # Parent 36e885190439a222868d809db59d1db8f363e39c clarified modules; diff -r 36e885190439 -r 833af0d6d469 src/Pure/Concurrent/bash.scala --- a/src/Pure/Concurrent/bash.scala Wed Feb 24 22:03:24 2016 +0100 +++ b/src/Pure/Concurrent/bash.scala Wed Feb 24 22:11:28 2016 +0100 @@ -13,36 +13,6 @@ object Bash { - /** result **/ - - final case class Result(out_lines: List[String], err_lines: List[String], rc: Int) - { - def out: String = cat_lines(out_lines) - def err: String = cat_lines(err_lines) - - def error(s: String, err_rc: Int = 0): Result = - copy(err_lines = err_lines ::: List(s), rc = rc max err_rc) - - def ok: Boolean = rc == 0 - def interrupted: Boolean = rc == Exn.Interrupt.return_code - - def check: Result = - if (ok) this - else if (interrupted) throw Exn.Interrupt() - else Library.error(err) - - def print: Result = - { - Output.warning(Library.trim_line(err)) - Output.writeln(Library.trim_line(out)) - Result(Nil, Nil, rc) - } - } - - - - /** process **/ - def process(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process = new Process(cwd, env, redirect, args:_*) diff -r 36e885190439 -r 833af0d6d469 src/Pure/System/isabelle_system.scala --- a/src/Pure/System/isabelle_system.scala Wed Feb 24 22:03:24 2016 +0100 +++ b/src/Pure/System/isabelle_system.scala Wed Feb 24 22:11:28 2016 +0100 @@ -319,7 +319,7 @@ progress_stdout: String => Unit = (_: String) => (), progress_stderr: String => Unit = (_: String) => (), progress_limit: Option[Long] = None, - strict: Boolean = true): Bash.Result = + strict: Boolean = true): Process_Result = { with_tmp_file("isabelle_script") { script_file => File.write(script_file, script) @@ -337,7 +337,7 @@ catch { case Exn.Interrupt() => proc.terminate; Exn.Interrupt.return_code } if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt() - Bash.Result(stdout.join, stderr.join, rc) + Process_Result(stdout.join, stderr.join, rc) } } @@ -367,10 +367,11 @@ def pdf_viewer(arg: Path): Unit = bash("exec \"$PDF_VIEWER\" '" + File.standard_path(arg) + "' >/dev/null 2>/dev/null &") - def hg(cmd_line: String, cwd: Path = Path.current): Bash.Result = + def hg(cmd_line: String, cwd: Path = Path.current): Process_Result = bash("cd " + File.shell_path(cwd) + " && \"${HG:-hg}\" " + cmd_line) + /** Isabelle resources **/ /* components */ diff -r 36e885190439 -r 833af0d6d469 src/Pure/System/process_result.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/System/process_result.scala Wed Feb 24 22:11:28 2016 +0100 @@ -0,0 +1,31 @@ +/* Title: Pure/System/process_result.scala + Author: Makarius + +Result of system process. +*/ + +package isabelle + +final case class Process_Result(out_lines: List[String], err_lines: List[String], rc: Int) +{ + def out: String = cat_lines(out_lines) + def err: String = cat_lines(err_lines) + + def error(s: String, err_rc: Int = 0): Process_Result = + copy(err_lines = err_lines ::: List(s), rc = rc max err_rc) + + def ok: Boolean = rc == 0 + def interrupted: Boolean = rc == Exn.Interrupt.return_code + + def check: Process_Result = + if (ok) this + else if (interrupted) throw Exn.Interrupt() + else Library.error(err) + + def print: Process_Result = + { + Output.warning(Library.trim_line(err)) + Output.writeln(Library.trim_line(out)) + Process_Result(Nil, Nil, rc) + } +} diff -r 36e885190439 -r 833af0d6d469 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Wed Feb 24 22:03:24 2016 +0100 +++ b/src/Pure/Tools/build.scala Wed Feb 24 22:11:28 2016 +0100 @@ -628,7 +628,7 @@ else None } - def join: Bash.Result = + def join: Process_Result = { val res = result.join diff -r 36e885190439 -r 833af0d6d469 src/Pure/build-jars --- a/src/Pure/build-jars Wed Feb 24 22:03:24 2016 +0100 +++ b/src/Pure/build-jars Wed Feb 24 22:11:28 2016 +0100 @@ -82,6 +82,7 @@ System/options.scala System/platform.scala System/posix_interrupt.scala + System/process_result.scala System/progress.scala System/system_channel.scala System/utf8.scala