--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/bash.scala Thu Aug 20 20:36:06 2015 +0200
@@ -0,0 +1,106 @@
+/* Title: Pure/Concurrent/bash.scala
+ Author: Makarius
+
+GNU bash processes, with propagation of interrupts.
+*/
+
+package isabelle
+
+
+import java.io.{File => JFile, BufferedReader, InputStreamReader,
+ BufferedWriter, OutputStreamWriter}
+
+
+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 add_err(s: String): Result = copy(err_lines = err_lines ::: List(s))
+ def set_rc(i: Int): Result = copy(rc = i)
+
+ def check_error: Result =
+ if (rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
+ else if (rc != 0) error(err)
+ else this
+ }
+
+
+
+ /** process **/
+
+ def process(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*): Process =
+ new Process(cwd, env, redirect, args:_*)
+
+ class Process private [Bash](
+ cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*)
+ extends Prover.System_Process
+ {
+ private val params =
+ List(File.standard_path(Path.explode("~~/lib/scripts/process")), "group", "-", "no_script")
+ private val proc = Isabelle_System.execute_env(cwd, env, redirect, (params ::: args.toList):_*)
+
+
+ // channels
+
+ val stdin: BufferedWriter =
+ new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, UTF8.charset))
+
+ val stdout: BufferedReader =
+ new BufferedReader(new InputStreamReader(proc.getInputStream, UTF8.charset))
+
+ val stderr: BufferedReader =
+ new BufferedReader(new InputStreamReader(proc.getErrorStream, UTF8.charset))
+
+
+ // signals
+
+ private val pid = stdout.readLine
+
+ private def kill_cmd(signal: String): Int =
+ Isabelle_System.execute(true, "/usr/bin/env", "bash", "-c", "kill -" + signal + " -" + pid)
+ .waitFor
+
+ private def kill(signal: String): Boolean =
+ Exn.Interrupt.postpone { kill_cmd(signal); kill_cmd("0") == 0 } getOrElse true
+
+ private def multi_kill(signal: String): Boolean =
+ {
+ var running = true
+ var count = 10
+ while (running && count > 0) {
+ if (kill(signal)) {
+ Exn.Interrupt.postpone {
+ Thread.sleep(100)
+ count -= 1
+ }
+ }
+ else running = false
+ }
+ running
+ }
+
+ def interrupt() { multi_kill("INT") }
+ def terminate() { multi_kill("INT") && multi_kill("TERM") && kill("KILL"); proc.destroy }
+
+
+ // JVM shutdown hook
+
+ private val shutdown_hook = new Thread { override def run = terminate() }
+
+ try { Runtime.getRuntime.addShutdownHook(shutdown_hook) }
+ catch { case _: IllegalStateException => }
+
+ private def cleanup() =
+ try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
+ catch { case _: IllegalStateException => }
+
+
+ /* result */
+
+ def join: Int = { val rc = proc.waitFor; cleanup(); rc }
+ }
+}
--- a/src/Pure/System/isabelle_process.scala Thu Aug 20 19:33:26 2015 +0200
+++ b/src/Pure/System/isabelle_process.scala Thu Aug 20 20:36:06 2015 +0200
@@ -19,9 +19,7 @@
val cmdline =
Isabelle_System.getenv_strict("ISABELLE_PROCESS") ::
(system_channel.prover_args ::: prover_args)
- val process =
- new Isabelle_System.Managed_Process(null, null, false, cmdline: _*) with
- Prover.System_Process
+ val process = Bash.process(null, null, false, cmdline: _*)
process.stdin.close
process
}
--- a/src/Pure/System/isabelle_system.scala Thu Aug 20 19:33:26 2015 +0200
+++ b/src/Pure/System/isabelle_system.scala Thu Aug 20 20:36:06 2015 +0200
@@ -9,8 +9,7 @@
import java.util.regex.Pattern
-import java.io.{File => JFile, BufferedReader, InputStreamReader,
- BufferedWriter, OutputStreamWriter, IOException}
+import java.io.{File => JFile, IOException}
import java.nio.file.{Path => JPath, Files, SimpleFileVisitor, FileVisitResult}
import java.nio.file.attribute.BasicFileAttributes
import java.net.{URL, URLDecoder, MalformedURLException}
@@ -294,75 +293,6 @@
execute_env(null, null, redirect, args: _*)
- /* managed process */
-
- class Managed_Process(cwd: JFile, env: Map[String, String], redirect: Boolean, args: String*)
- {
- private val params =
- List(File.standard_path(Path.explode("~~/lib/scripts/process")), "group", "-", "no_script")
- private val proc = execute_env(cwd, env, redirect, (params ::: args.toList):_*)
-
-
- // channels
-
- val stdin: BufferedWriter =
- new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, UTF8.charset))
-
- val stdout: BufferedReader =
- new BufferedReader(new InputStreamReader(proc.getInputStream, UTF8.charset))
-
- val stderr: BufferedReader =
- new BufferedReader(new InputStreamReader(proc.getErrorStream, UTF8.charset))
-
-
- // signals
-
- private val pid = stdout.readLine
-
- private def kill_cmd(signal: String): Int =
- execute(true, "/usr/bin/env", "bash", "-c", "kill -" + signal + " -" + pid).waitFor
-
- private def kill(signal: String): Boolean =
- Exn.Interrupt.postpone { kill_cmd(signal); kill_cmd("0") == 0 } getOrElse true
-
- private def multi_kill(signal: String): Boolean =
- {
- var running = true
- var count = 10
- while (running && count > 0) {
- if (kill(signal)) {
- Exn.Interrupt.postpone {
- Thread.sleep(100)
- count -= 1
- }
- }
- else running = false
- }
- running
- }
-
- def interrupt() { multi_kill("INT") }
- def terminate() { multi_kill("INT") && multi_kill("TERM") && kill("KILL"); proc.destroy }
-
-
- // JVM shutdown hook
-
- private val shutdown_hook = new Thread { override def run = terminate() }
-
- try { Runtime.getRuntime.addShutdownHook(shutdown_hook) }
- catch { case _: IllegalStateException => }
-
- private def cleanup() =
- try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
- catch { case _: IllegalStateException => }
-
-
- /* result */
-
- def join: Int = { val rc = proc.waitFor; cleanup(); rc }
- }
-
-
/* tmp files */
private def isabelle_tmp_prefix(): JFile =
@@ -430,20 +360,7 @@
/* bash */
- final case class Bash_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 add_err(s: String): Bash_Result = copy(err_lines = err_lines ::: List(s))
- def set_rc(i: Int): Bash_Result = copy(rc = i)
-
- def check_error: Bash_Result =
- if (rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
- else if (rc != 0) error(err)
- else this
- }
-
- private class Limited_Progress(proc: Managed_Process, progress_limit: Option[Long])
+ private class Limited_Progress(proc: Bash.Process, progress_limit: Option[Long])
{
private var count = 0L
def apply(progress: String => Unit)(line: String): Unit = synchronized {
@@ -460,11 +377,11 @@
progress_stdout: String => Unit = (_: String) => (),
progress_stderr: String => Unit = (_: String) => (),
progress_limit: Option[Long] = None,
- strict: Boolean = true): Bash_Result =
+ strict: Boolean = true): Bash.Result =
{
with_tmp_file("isabelle_script") { script_file =>
File.write(script_file, script)
- val proc = new Managed_Process(cwd, env, false, "bash", posix_path(script_file))
+ val proc = Bash.process(cwd, env, false, "bash", posix_path(script_file))
proc.stdin.close
val limited = new Limited_Progress(proc, progress_limit)
@@ -482,11 +399,11 @@
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)
+ Bash.Result(stdout.join, stderr.join, rc)
}
}
- def bash(script: String): Bash_Result = bash_env(null, null, script)
+ def bash(script: String): Bash.Result = bash_env(null, null, script)
/* system tools */
@@ -514,7 +431,7 @@
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): Bash.Result =
bash("cd " + File.shell_path(cwd) + " && \"${HG:-hg}\" " + cmd_line)
--- a/src/Pure/Tools/build.scala Thu Aug 20 19:33:26 2015 +0200
+++ b/src/Pure/Tools/build.scala Thu Aug 20 20:36:06 2015 +0200
@@ -653,7 +653,7 @@
else None
}
- def join: Isabelle_System.Bash_Result =
+ def join: Bash.Result =
{
val res = result.join
--- a/src/Pure/build-jars Thu Aug 20 19:33:26 2015 +0200
+++ b/src/Pure/build-jars Thu Aug 20 20:36:06 2015 +0200
@@ -9,6 +9,7 @@
## sources
declare -a SOURCES=(
+ Concurrent/bash.scala
Concurrent/consumer_thread.scala
Concurrent/counter.scala
Concurrent/event_timer.scala