clarified files;
authorwenzelm
Thu Mar 10 09:50:53 2016 +0100 (2016-03-10)
changeset 625846cd36a0d2a28
parent 62579 bfa38c2e751f
child 62585 5d4ed917450d
clarified files;
src/Pure/Concurrent/bash.ML
src/Pure/Concurrent/bash.scala
src/Pure/Concurrent/bash_windows.ML
src/Pure/ROOT
src/Pure/ROOT.ML
src/Pure/System/bash.ML
src/Pure/System/bash.scala
src/Pure/System/bash_windows.ML
src/Pure/build-jars
     1.1 --- a/src/Pure/Concurrent/bash.ML	Wed Mar 09 21:01:22 2016 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,102 +0,0 @@
     1.4 -(*  Title:      Pure/Concurrent/bash.ML
     1.5 -    Author:     Makarius
     1.6 -
     1.7 -GNU bash processes, with propagation of interrupts -- POSIX version.
     1.8 -*)
     1.9 -
    1.10 -signature BASH =
    1.11 -sig
    1.12 -  val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit}
    1.13 -end;
    1.14 -
    1.15 -structure Bash: BASH =
    1.16 -struct
    1.17 -
    1.18 -val process = uninterruptible (fn restore_attributes => fn script =>
    1.19 -  let
    1.20 -    datatype result = Wait | Signal | Result of int;
    1.21 -    val result = Synchronized.var "bash_result" Wait;
    1.22 -
    1.23 -    val id = serial_string ();
    1.24 -    val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
    1.25 -    val out_path = File.tmp_path (Path.basic ("bash_out" ^ id));
    1.26 -    val err_path = File.tmp_path (Path.basic ("bash_err" ^ id));
    1.27 -    val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id));
    1.28 -
    1.29 -    fun cleanup_files () =
    1.30 -     (try File.rm script_path;
    1.31 -      try File.rm out_path;
    1.32 -      try File.rm err_path;
    1.33 -      try File.rm pid_path);
    1.34 -    val _ = cleanup_files ();
    1.35 -
    1.36 -    val system_thread =
    1.37 -      Standard_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () =>
    1.38 -        Multithreading.with_attributes Multithreading.private_interrupts (fn _ =>
    1.39 -          let
    1.40 -            val _ = File.write script_path script;
    1.41 -            val _ = getenv_strict "ISABELLE_BASH_PROCESS";
    1.42 -            val status =
    1.43 -              OS.Process.system
    1.44 -                ("exec \"$ISABELLE_BASH_PROCESS\" " ^ File.bash_path pid_path ^ " \"\"" ^
    1.45 -                  " bash " ^ File.bash_path script_path ^
    1.46 -                  " > " ^ File.bash_path out_path ^
    1.47 -                  " 2> " ^ File.bash_path err_path);
    1.48 -            val res =
    1.49 -              (case Posix.Process.fromStatus status of
    1.50 -                Posix.Process.W_EXITED => Result 0
    1.51 -              | Posix.Process.W_EXITSTATUS 0wx82 => Signal
    1.52 -              | Posix.Process.W_EXITSTATUS w => Result (Word8.toInt w)
    1.53 -              | Posix.Process.W_SIGNALED s =>
    1.54 -                  if s = Posix.Signal.int then Signal
    1.55 -                  else Result (256 + LargeWord.toInt (Posix.Signal.toWord s))
    1.56 -              | Posix.Process.W_STOPPED s =>
    1.57 -                  Result (512 + LargeWord.toInt (Posix.Signal.toWord s)));
    1.58 -          in Synchronized.change result (K res) end
    1.59 -          handle exn =>
    1.60 -            (Synchronized.change result (fn Wait => Signal | res => res); Exn.reraise exn)));
    1.61 -
    1.62 -    fun read_pid 0 = NONE
    1.63 -      | read_pid count =
    1.64 -          (case (Int.fromString (File.read pid_path) handle IO.Io _ => NONE) of
    1.65 -            NONE => (OS.Process.sleep (seconds 0.1); read_pid (count - 1))
    1.66 -          | some => some);
    1.67 -
    1.68 -    fun terminate NONE = ()
    1.69 -      | terminate (SOME pid) =
    1.70 -          let
    1.71 -            fun kill s =
    1.72 -              (Posix.Process.kill
    1.73 -                (Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid)), s); true)
    1.74 -              handle OS.SysErr _ => false;
    1.75 -
    1.76 -            fun multi_kill count s =
    1.77 -              count = 0 orelse
    1.78 -                (kill s; kill (Posix.Signal.fromWord 0w0)) andalso
    1.79 -                (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s);
    1.80 -            val _ =
    1.81 -              multi_kill 10 Posix.Signal.int andalso
    1.82 -              multi_kill 10 Posix.Signal.term andalso
    1.83 -              multi_kill 10 Posix.Signal.kill;
    1.84 -          in () end;
    1.85 -
    1.86 -    fun cleanup () =
    1.87 -     (Standard_Thread.interrupt_unsynchronized system_thread;
    1.88 -      cleanup_files ());
    1.89 -  in
    1.90 -    let
    1.91 -      val _ =
    1.92 -        restore_attributes (fn () =>
    1.93 -          Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) ();
    1.94 -
    1.95 -      val out = the_default "" (try File.read out_path);
    1.96 -      val err = the_default "" (try File.read err_path);
    1.97 -      val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc);
    1.98 -      val pid = read_pid 1;
    1.99 -      val _ = cleanup ();
   1.100 -    in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end
   1.101 -    handle exn => (terminate (read_pid 10); cleanup (); Exn.reraise exn)
   1.102 -  end);
   1.103 -
   1.104 -end;
   1.105 -
     2.1 --- a/src/Pure/Concurrent/bash.scala	Wed Mar 09 21:01:22 2016 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,168 +0,0 @@
     2.4 -/*  Title:      Pure/Concurrent/bash.scala
     2.5 -    Author:     Makarius
     2.6 -
     2.7 -GNU bash processes, with propagation of interrupts.
     2.8 -*/
     2.9 -
    2.10 -package isabelle
    2.11 -
    2.12 -
    2.13 -import java.io.{File => JFile, BufferedReader, InputStreamReader,
    2.14 -  BufferedWriter, OutputStreamWriter}
    2.15 -
    2.16 -
    2.17 -object Bash
    2.18 -{
    2.19 -  private class Limited_Progress(proc: Process, progress_limit: Option[Long])
    2.20 -  {
    2.21 -    private var count = 0L
    2.22 -    def apply(progress: String => Unit)(line: String): Unit = synchronized {
    2.23 -      progress(line)
    2.24 -      count = count + line.length + 1
    2.25 -      progress_limit match {
    2.26 -        case Some(limit) if count > limit => proc.terminate
    2.27 -        case _ =>
    2.28 -      }
    2.29 -    }
    2.30 -  }
    2.31 -
    2.32 -  def process(script: String,
    2.33 -      cwd: JFile = null,
    2.34 -      env: Map[String, String] = Map.empty,
    2.35 -      redirect: Boolean = false): Process =
    2.36 -    new Process(script, cwd, env, redirect)
    2.37 -
    2.38 -  class Process private [Bash](
    2.39 -      script: String, cwd: JFile, env: Map[String, String], redirect: Boolean)
    2.40 -    extends Prover.System_Process
    2.41 -  {
    2.42 -    private val timing_file = Isabelle_System.tmp_file("bash_script")
    2.43 -    private val timing = Synchronized[Option[Timing]](None)
    2.44 -
    2.45 -    private val script_file = Isabelle_System.tmp_file("bash_script")
    2.46 -    File.write(script_file, script)
    2.47 -
    2.48 -    private val proc =
    2.49 -      Isabelle_System.process(cwd, Isabelle_System.settings(env), redirect,
    2.50 -        File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")), "-",
    2.51 -          File.standard_path(timing_file), "bash", File.standard_path(script_file))
    2.52 -
    2.53 -
    2.54 -    // channels
    2.55 -
    2.56 -    val stdin: BufferedWriter =
    2.57 -      new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, UTF8.charset))
    2.58 -
    2.59 -    val stdout: BufferedReader =
    2.60 -      new BufferedReader(new InputStreamReader(proc.getInputStream, UTF8.charset))
    2.61 -
    2.62 -    val stderr: BufferedReader =
    2.63 -      new BufferedReader(new InputStreamReader(proc.getErrorStream, UTF8.charset))
    2.64 -
    2.65 -
    2.66 -    // signals
    2.67 -
    2.68 -    private val pid = stdout.readLine
    2.69 -
    2.70 -    def interrupt()
    2.71 -    { Exn.Interrupt.postpone { Isabelle_System.kill("INT", pid) } }
    2.72 -
    2.73 -    private def kill(signal: String): Boolean =
    2.74 -      Exn.Interrupt.postpone {
    2.75 -        Isabelle_System.kill(signal, pid)
    2.76 -        Isabelle_System.kill("0", pid)._2 == 0 } getOrElse true
    2.77 -
    2.78 -    private def multi_kill(signal: String): Boolean =
    2.79 -    {
    2.80 -      var running = true
    2.81 -      var count = 10
    2.82 -      while (running && count > 0) {
    2.83 -        if (kill(signal)) {
    2.84 -          Exn.Interrupt.postpone {
    2.85 -            Thread.sleep(100)
    2.86 -            count -= 1
    2.87 -          }
    2.88 -        }
    2.89 -        else running = false
    2.90 -      }
    2.91 -      running
    2.92 -    }
    2.93 -
    2.94 -    def terminate()
    2.95 -    {
    2.96 -      multi_kill("INT") && multi_kill("TERM") && kill("KILL")
    2.97 -      proc.destroy
    2.98 -      cleanup()
    2.99 -    }
   2.100 -
   2.101 -
   2.102 -    // JVM shutdown hook
   2.103 -
   2.104 -    private val shutdown_hook = new Thread { override def run = terminate() }
   2.105 -
   2.106 -    try { Runtime.getRuntime.addShutdownHook(shutdown_hook) }
   2.107 -    catch { case _: IllegalStateException => }
   2.108 -
   2.109 -
   2.110 -    // cleanup
   2.111 -
   2.112 -    private def cleanup()
   2.113 -    {
   2.114 -      try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
   2.115 -      catch { case _: IllegalStateException => }
   2.116 -
   2.117 -      script_file.delete
   2.118 -
   2.119 -      timing.change {
   2.120 -        case None =>
   2.121 -          if (timing_file.isFile) {
   2.122 -            val t =
   2.123 -              Word.explode(File.read(timing_file)) match {
   2.124 -                case List(Properties.Value.Long(elapsed), Properties.Value.Long(cpu)) =>
   2.125 -                  Timing(Time.ms(elapsed), Time.ms(cpu), Time.zero)
   2.126 -                case _ => Timing.zero
   2.127 -              }
   2.128 -            timing_file.delete
   2.129 -            Some(t)
   2.130 -          }
   2.131 -          else Some(Timing.zero)
   2.132 -        case some => some
   2.133 -      }
   2.134 -    }
   2.135 -
   2.136 -
   2.137 -    // join
   2.138 -
   2.139 -    def join: Int =
   2.140 -    {
   2.141 -      val rc = proc.waitFor
   2.142 -      cleanup()
   2.143 -      rc
   2.144 -    }
   2.145 -
   2.146 -
   2.147 -    // result
   2.148 -
   2.149 -    def result(
   2.150 -      progress_stdout: String => Unit = (_: String) => (),
   2.151 -      progress_stderr: String => Unit = (_: String) => (),
   2.152 -      progress_limit: Option[Long] = None,
   2.153 -      strict: Boolean = true): Process_Result =
   2.154 -    {
   2.155 -      stdin.close
   2.156 -
   2.157 -      val limited = new Limited_Progress(this, progress_limit)
   2.158 -      val out_lines =
   2.159 -        Future.thread("bash_stdout") { File.read_lines(stdout, limited(progress_stdout)) }
   2.160 -      val err_lines =
   2.161 -        Future.thread("bash_stderr") { File.read_lines(stderr, limited(progress_stderr)) }
   2.162 -
   2.163 -      val rc =
   2.164 -        try { join }
   2.165 -        catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code }
   2.166 -      if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
   2.167 -
   2.168 -      Process_Result(rc, out_lines.join, err_lines.join, false, timing.value getOrElse Timing.zero)
   2.169 -    }
   2.170 -  }
   2.171 -}
     3.1 --- a/src/Pure/Concurrent/bash_windows.ML	Wed Mar 09 21:01:22 2016 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,99 +0,0 @@
     3.4 -(*  Title:      Pure/Concurrent/bash_windows.ML
     3.5 -    Author:     Makarius
     3.6 -
     3.7 -GNU bash processes, with propagation of interrupts -- Windows version.
     3.8 -*)
     3.9 -
    3.10 -signature BASH =
    3.11 -sig
    3.12 -  val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit}
    3.13 -end;
    3.14 -
    3.15 -structure Bash: BASH =
    3.16 -struct
    3.17 -
    3.18 -val process = uninterruptible (fn restore_attributes => fn script =>
    3.19 -  let
    3.20 -    datatype result = Wait | Signal | Result of int;
    3.21 -    val result = Synchronized.var "bash_result" Wait;
    3.22 -
    3.23 -    val id = serial_string ();
    3.24 -    val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
    3.25 -    val out_path = File.tmp_path (Path.basic ("bash_out" ^ id));
    3.26 -    val err_path = File.tmp_path (Path.basic ("bash_err" ^ id));
    3.27 -    val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id));
    3.28 -
    3.29 -    fun cleanup_files () =
    3.30 -     (try File.rm script_path;
    3.31 -      try File.rm out_path;
    3.32 -      try File.rm err_path;
    3.33 -      try File.rm pid_path);
    3.34 -    val _ = cleanup_files ();
    3.35 -
    3.36 -    val system_thread =
    3.37 -      Standard_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () =>
    3.38 -        Multithreading.with_attributes Multithreading.private_interrupts (fn _ =>
    3.39 -          let
    3.40 -            val _ = File.write script_path script;
    3.41 -            val bash_script =
    3.42 -              "bash " ^ File.bash_path script_path ^
    3.43 -                " > " ^ File.bash_path out_path ^
    3.44 -                " 2> " ^ File.bash_path err_path;
    3.45 -            val bash_process = getenv_strict "ISABELLE_BASH_PROCESS";
    3.46 -            val rc =
    3.47 -              Windows.simpleExecute ("",
    3.48 -                quote (ML_System.platform_path bash_process) ^ " " ^
    3.49 -                quote (File.platform_path pid_path) ^  " \"\" bash -c " ^ quote bash_script)
    3.50 -              |> Windows.fromStatus |> SysWord.toInt;
    3.51 -            val res = if rc = 130 orelse rc = 512 then Signal else Result rc;
    3.52 -          in Synchronized.change result (K res) end
    3.53 -          handle exn =>
    3.54 -            (Synchronized.change result (fn Wait => Signal | res => res); Exn.reraise exn)));
    3.55 -
    3.56 -    fun read_pid 0 = NONE
    3.57 -      | read_pid count =
    3.58 -          (case (Int.fromString (File.read pid_path) handle IO.Io _ => NONE) of
    3.59 -            NONE => (OS.Process.sleep (seconds 0.1); read_pid (count - 1))
    3.60 -          | some => some);
    3.61 -
    3.62 -    fun terminate NONE = ()
    3.63 -      | terminate (SOME pid) =
    3.64 -          let
    3.65 -            fun kill s =
    3.66 -              let
    3.67 -                val cmd = getenv_strict "CYGWIN_ROOT" ^ "\\bin\\bash.exe";
    3.68 -                val arg = "kill -" ^ s ^ " -" ^ string_of_int pid;
    3.69 -              in
    3.70 -                OS.Process.isSuccess (Windows.simpleExecute ("", quote cmd ^ " -c " ^ quote arg))
    3.71 -                  handle OS.SysErr _ => false
    3.72 -              end;
    3.73 -
    3.74 -            fun multi_kill count s =
    3.75 -              count = 0 orelse
    3.76 -                (kill s; kill "0") andalso
    3.77 -                (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s);
    3.78 -            val _ =
    3.79 -              multi_kill 10 "INT" andalso
    3.80 -              multi_kill 10 "TERM" andalso
    3.81 -              multi_kill 10 "KILL";
    3.82 -          in () end;
    3.83 -
    3.84 -    fun cleanup () =
    3.85 -     (Standard_Thread.interrupt_unsynchronized system_thread;
    3.86 -      cleanup_files ());
    3.87 -  in
    3.88 -    let
    3.89 -      val _ =
    3.90 -        restore_attributes (fn () =>
    3.91 -          Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) ();
    3.92 -
    3.93 -      val out = the_default "" (try File.read out_path);
    3.94 -      val err = the_default "" (try File.read err_path);
    3.95 -      val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc);
    3.96 -      val pid = read_pid 1;
    3.97 -      val _ = cleanup ();
    3.98 -    in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end
    3.99 -    handle exn => (terminate (read_pid 10); cleanup (); Exn.reraise exn)
   3.100 -  end);
   3.101 -
   3.102 -end;
     4.1 --- a/src/Pure/ROOT	Wed Mar 09 21:01:22 2016 +0100
     4.2 +++ b/src/Pure/ROOT	Thu Mar 10 09:50:53 2016 +0100
     4.3 @@ -3,8 +3,6 @@
     4.4  session Pure =
     4.5    global_theories Pure
     4.6    files
     4.7 -    "Concurrent/bash.ML"
     4.8 -    "Concurrent/bash_windows.ML"
     4.9      "Concurrent/cache.ML"
    4.10      "Concurrent/counter.ML"
    4.11      "Concurrent/event_timer.ML"
    4.12 @@ -153,6 +151,8 @@
    4.13      "Syntax/syntax_trans.ML"
    4.14      "Syntax/term_position.ML"
    4.15      "Syntax/type_annotation.ML"
    4.16 +    "System/bash.ML"
    4.17 +    "System/bash_windows.ML"
    4.18      "System/command_line.ML"
    4.19      "System/invoke_scala.ML"
    4.20      "System/isabelle_process.ML"
     5.1 --- a/src/Pure/ROOT.ML	Wed Mar 09 21:01:22 2016 +0100
     5.2 +++ b/src/Pure/ROOT.ML	Thu Mar 10 09:50:53 2016 +0100
     5.3 @@ -193,10 +193,6 @@
     5.4  use "Concurrent/standard_thread.ML";
     5.5  use "Concurrent/single_assignment.ML";
     5.6  
     5.7 -if ML_System.platform_is_windows
     5.8 -then use "Concurrent/bash_windows.ML"
     5.9 -else use "Concurrent/bash.ML";
    5.10 -
    5.11  use "Concurrent/par_exn.ML";
    5.12  use "Concurrent/task_queue.ML";
    5.13  use "Concurrent/future.ML";
    5.14 @@ -371,8 +367,13 @@
    5.15  use "Proof/proof_checker.ML";
    5.16  use "Proof/extraction.ML";
    5.17  
    5.18 +(*Isabelle system*)
    5.19 +if ML_System.platform_is_windows
    5.20 +then use "System/bash_windows.ML"
    5.21 +else use "System/bash.ML";
    5.22 +use "System/isabelle_system.ML";
    5.23 +
    5.24  (*theory documents*)
    5.25 -use "System/isabelle_system.ML";
    5.26  use "Thy/term_style.ML";
    5.27  use "Isar/outer_syntax.ML";
    5.28  use "Thy/thy_output.ML";
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/src/Pure/System/bash.ML	Thu Mar 10 09:50:53 2016 +0100
     6.3 @@ -0,0 +1,102 @@
     6.4 +(*  Title:      Pure/System/bash.ML
     6.5 +    Author:     Makarius
     6.6 +
     6.7 +GNU bash processes, with propagation of interrupts -- POSIX version.
     6.8 +*)
     6.9 +
    6.10 +signature BASH =
    6.11 +sig
    6.12 +  val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit}
    6.13 +end;
    6.14 +
    6.15 +structure Bash: BASH =
    6.16 +struct
    6.17 +
    6.18 +val process = uninterruptible (fn restore_attributes => fn script =>
    6.19 +  let
    6.20 +    datatype result = Wait | Signal | Result of int;
    6.21 +    val result = Synchronized.var "bash_result" Wait;
    6.22 +
    6.23 +    val id = serial_string ();
    6.24 +    val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
    6.25 +    val out_path = File.tmp_path (Path.basic ("bash_out" ^ id));
    6.26 +    val err_path = File.tmp_path (Path.basic ("bash_err" ^ id));
    6.27 +    val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id));
    6.28 +
    6.29 +    fun cleanup_files () =
    6.30 +     (try File.rm script_path;
    6.31 +      try File.rm out_path;
    6.32 +      try File.rm err_path;
    6.33 +      try File.rm pid_path);
    6.34 +    val _ = cleanup_files ();
    6.35 +
    6.36 +    val system_thread =
    6.37 +      Standard_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () =>
    6.38 +        Multithreading.with_attributes Multithreading.private_interrupts (fn _ =>
    6.39 +          let
    6.40 +            val _ = File.write script_path script;
    6.41 +            val _ = getenv_strict "ISABELLE_BASH_PROCESS";
    6.42 +            val status =
    6.43 +              OS.Process.system
    6.44 +                ("exec \"$ISABELLE_BASH_PROCESS\" " ^ File.bash_path pid_path ^ " \"\"" ^
    6.45 +                  " bash " ^ File.bash_path script_path ^
    6.46 +                  " > " ^ File.bash_path out_path ^
    6.47 +                  " 2> " ^ File.bash_path err_path);
    6.48 +            val res =
    6.49 +              (case Posix.Process.fromStatus status of
    6.50 +                Posix.Process.W_EXITED => Result 0
    6.51 +              | Posix.Process.W_EXITSTATUS 0wx82 => Signal
    6.52 +              | Posix.Process.W_EXITSTATUS w => Result (Word8.toInt w)
    6.53 +              | Posix.Process.W_SIGNALED s =>
    6.54 +                  if s = Posix.Signal.int then Signal
    6.55 +                  else Result (256 + LargeWord.toInt (Posix.Signal.toWord s))
    6.56 +              | Posix.Process.W_STOPPED s =>
    6.57 +                  Result (512 + LargeWord.toInt (Posix.Signal.toWord s)));
    6.58 +          in Synchronized.change result (K res) end
    6.59 +          handle exn =>
    6.60 +            (Synchronized.change result (fn Wait => Signal | res => res); Exn.reraise exn)));
    6.61 +
    6.62 +    fun read_pid 0 = NONE
    6.63 +      | read_pid count =
    6.64 +          (case (Int.fromString (File.read pid_path) handle IO.Io _ => NONE) of
    6.65 +            NONE => (OS.Process.sleep (seconds 0.1); read_pid (count - 1))
    6.66 +          | some => some);
    6.67 +
    6.68 +    fun terminate NONE = ()
    6.69 +      | terminate (SOME pid) =
    6.70 +          let
    6.71 +            fun kill s =
    6.72 +              (Posix.Process.kill
    6.73 +                (Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid)), s); true)
    6.74 +              handle OS.SysErr _ => false;
    6.75 +
    6.76 +            fun multi_kill count s =
    6.77 +              count = 0 orelse
    6.78 +                (kill s; kill (Posix.Signal.fromWord 0w0)) andalso
    6.79 +                (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s);
    6.80 +            val _ =
    6.81 +              multi_kill 10 Posix.Signal.int andalso
    6.82 +              multi_kill 10 Posix.Signal.term andalso
    6.83 +              multi_kill 10 Posix.Signal.kill;
    6.84 +          in () end;
    6.85 +
    6.86 +    fun cleanup () =
    6.87 +     (Standard_Thread.interrupt_unsynchronized system_thread;
    6.88 +      cleanup_files ());
    6.89 +  in
    6.90 +    let
    6.91 +      val _ =
    6.92 +        restore_attributes (fn () =>
    6.93 +          Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) ();
    6.94 +
    6.95 +      val out = the_default "" (try File.read out_path);
    6.96 +      val err = the_default "" (try File.read err_path);
    6.97 +      val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc);
    6.98 +      val pid = read_pid 1;
    6.99 +      val _ = cleanup ();
   6.100 +    in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end
   6.101 +    handle exn => (terminate (read_pid 10); cleanup (); Exn.reraise exn)
   6.102 +  end);
   6.103 +
   6.104 +end;
   6.105 +
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/Pure/System/bash.scala	Thu Mar 10 09:50:53 2016 +0100
     7.3 @@ -0,0 +1,168 @@
     7.4 +/*  Title:      Pure/System/bash.scala
     7.5 +    Author:     Makarius
     7.6 +
     7.7 +GNU bash processes, with propagation of interrupts.
     7.8 +*/
     7.9 +
    7.10 +package isabelle
    7.11 +
    7.12 +
    7.13 +import java.io.{File => JFile, BufferedReader, InputStreamReader,
    7.14 +  BufferedWriter, OutputStreamWriter}
    7.15 +
    7.16 +
    7.17 +object Bash
    7.18 +{
    7.19 +  private class Limited_Progress(proc: Process, progress_limit: Option[Long])
    7.20 +  {
    7.21 +    private var count = 0L
    7.22 +    def apply(progress: String => Unit)(line: String): Unit = synchronized {
    7.23 +      progress(line)
    7.24 +      count = count + line.length + 1
    7.25 +      progress_limit match {
    7.26 +        case Some(limit) if count > limit => proc.terminate
    7.27 +        case _ =>
    7.28 +      }
    7.29 +    }
    7.30 +  }
    7.31 +
    7.32 +  def process(script: String,
    7.33 +      cwd: JFile = null,
    7.34 +      env: Map[String, String] = Map.empty,
    7.35 +      redirect: Boolean = false): Process =
    7.36 +    new Process(script, cwd, env, redirect)
    7.37 +
    7.38 +  class Process private [Bash](
    7.39 +      script: String, cwd: JFile, env: Map[String, String], redirect: Boolean)
    7.40 +    extends Prover.System_Process
    7.41 +  {
    7.42 +    private val timing_file = Isabelle_System.tmp_file("bash_script")
    7.43 +    private val timing = Synchronized[Option[Timing]](None)
    7.44 +
    7.45 +    private val script_file = Isabelle_System.tmp_file("bash_script")
    7.46 +    File.write(script_file, script)
    7.47 +
    7.48 +    private val proc =
    7.49 +      Isabelle_System.process(cwd, Isabelle_System.settings(env), redirect,
    7.50 +        File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")), "-",
    7.51 +          File.standard_path(timing_file), "bash", File.standard_path(script_file))
    7.52 +
    7.53 +
    7.54 +    // channels
    7.55 +
    7.56 +    val stdin: BufferedWriter =
    7.57 +      new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, UTF8.charset))
    7.58 +
    7.59 +    val stdout: BufferedReader =
    7.60 +      new BufferedReader(new InputStreamReader(proc.getInputStream, UTF8.charset))
    7.61 +
    7.62 +    val stderr: BufferedReader =
    7.63 +      new BufferedReader(new InputStreamReader(proc.getErrorStream, UTF8.charset))
    7.64 +
    7.65 +
    7.66 +    // signals
    7.67 +
    7.68 +    private val pid = stdout.readLine
    7.69 +
    7.70 +    def interrupt()
    7.71 +    { Exn.Interrupt.postpone { Isabelle_System.kill("INT", pid) } }
    7.72 +
    7.73 +    private def kill(signal: String): Boolean =
    7.74 +      Exn.Interrupt.postpone {
    7.75 +        Isabelle_System.kill(signal, pid)
    7.76 +        Isabelle_System.kill("0", pid)._2 == 0 } getOrElse true
    7.77 +
    7.78 +    private def multi_kill(signal: String): Boolean =
    7.79 +    {
    7.80 +      var running = true
    7.81 +      var count = 10
    7.82 +      while (running && count > 0) {
    7.83 +        if (kill(signal)) {
    7.84 +          Exn.Interrupt.postpone {
    7.85 +            Thread.sleep(100)
    7.86 +            count -= 1
    7.87 +          }
    7.88 +        }
    7.89 +        else running = false
    7.90 +      }
    7.91 +      running
    7.92 +    }
    7.93 +
    7.94 +    def terminate()
    7.95 +    {
    7.96 +      multi_kill("INT") && multi_kill("TERM") && kill("KILL")
    7.97 +      proc.destroy
    7.98 +      cleanup()
    7.99 +    }
   7.100 +
   7.101 +
   7.102 +    // JVM shutdown hook
   7.103 +
   7.104 +    private val shutdown_hook = new Thread { override def run = terminate() }
   7.105 +
   7.106 +    try { Runtime.getRuntime.addShutdownHook(shutdown_hook) }
   7.107 +    catch { case _: IllegalStateException => }
   7.108 +
   7.109 +
   7.110 +    // cleanup
   7.111 +
   7.112 +    private def cleanup()
   7.113 +    {
   7.114 +      try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
   7.115 +      catch { case _: IllegalStateException => }
   7.116 +
   7.117 +      script_file.delete
   7.118 +
   7.119 +      timing.change {
   7.120 +        case None =>
   7.121 +          if (timing_file.isFile) {
   7.122 +            val t =
   7.123 +              Word.explode(File.read(timing_file)) match {
   7.124 +                case List(Properties.Value.Long(elapsed), Properties.Value.Long(cpu)) =>
   7.125 +                  Timing(Time.ms(elapsed), Time.ms(cpu), Time.zero)
   7.126 +                case _ => Timing.zero
   7.127 +              }
   7.128 +            timing_file.delete
   7.129 +            Some(t)
   7.130 +          }
   7.131 +          else Some(Timing.zero)
   7.132 +        case some => some
   7.133 +      }
   7.134 +    }
   7.135 +
   7.136 +
   7.137 +    // join
   7.138 +
   7.139 +    def join: Int =
   7.140 +    {
   7.141 +      val rc = proc.waitFor
   7.142 +      cleanup()
   7.143 +      rc
   7.144 +    }
   7.145 +
   7.146 +
   7.147 +    // result
   7.148 +
   7.149 +    def result(
   7.150 +      progress_stdout: String => Unit = (_: String) => (),
   7.151 +      progress_stderr: String => Unit = (_: String) => (),
   7.152 +      progress_limit: Option[Long] = None,
   7.153 +      strict: Boolean = true): Process_Result =
   7.154 +    {
   7.155 +      stdin.close
   7.156 +
   7.157 +      val limited = new Limited_Progress(this, progress_limit)
   7.158 +      val out_lines =
   7.159 +        Future.thread("bash_stdout") { File.read_lines(stdout, limited(progress_stdout)) }
   7.160 +      val err_lines =
   7.161 +        Future.thread("bash_stderr") { File.read_lines(stderr, limited(progress_stderr)) }
   7.162 +
   7.163 +      val rc =
   7.164 +        try { join }
   7.165 +        catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code }
   7.166 +      if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
   7.167 +
   7.168 +      Process_Result(rc, out_lines.join, err_lines.join, false, timing.value getOrElse Timing.zero)
   7.169 +    }
   7.170 +  }
   7.171 +}
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/Pure/System/bash_windows.ML	Thu Mar 10 09:50:53 2016 +0100
     8.3 @@ -0,0 +1,99 @@
     8.4 +(*  Title:      Pure/Concurrent/bash_windows.ML
     8.5 +    Author:     Makarius
     8.6 +
     8.7 +GNU bash processes, with propagation of interrupts -- Windows version.
     8.8 +*)
     8.9 +
    8.10 +signature BASH =
    8.11 +sig
    8.12 +  val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit}
    8.13 +end;
    8.14 +
    8.15 +structure Bash: BASH =
    8.16 +struct
    8.17 +
    8.18 +val process = uninterruptible (fn restore_attributes => fn script =>
    8.19 +  let
    8.20 +    datatype result = Wait | Signal | Result of int;
    8.21 +    val result = Synchronized.var "bash_result" Wait;
    8.22 +
    8.23 +    val id = serial_string ();
    8.24 +    val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
    8.25 +    val out_path = File.tmp_path (Path.basic ("bash_out" ^ id));
    8.26 +    val err_path = File.tmp_path (Path.basic ("bash_err" ^ id));
    8.27 +    val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id));
    8.28 +
    8.29 +    fun cleanup_files () =
    8.30 +     (try File.rm script_path;
    8.31 +      try File.rm out_path;
    8.32 +      try File.rm err_path;
    8.33 +      try File.rm pid_path);
    8.34 +    val _ = cleanup_files ();
    8.35 +
    8.36 +    val system_thread =
    8.37 +      Standard_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () =>
    8.38 +        Multithreading.with_attributes Multithreading.private_interrupts (fn _ =>
    8.39 +          let
    8.40 +            val _ = File.write script_path script;
    8.41 +            val bash_script =
    8.42 +              "bash " ^ File.bash_path script_path ^
    8.43 +                " > " ^ File.bash_path out_path ^
    8.44 +                " 2> " ^ File.bash_path err_path;
    8.45 +            val bash_process = getenv_strict "ISABELLE_BASH_PROCESS";
    8.46 +            val rc =
    8.47 +              Windows.simpleExecute ("",
    8.48 +                quote (ML_System.platform_path bash_process) ^ " " ^
    8.49 +                quote (File.platform_path pid_path) ^  " \"\" bash -c " ^ quote bash_script)
    8.50 +              |> Windows.fromStatus |> SysWord.toInt;
    8.51 +            val res = if rc = 130 orelse rc = 512 then Signal else Result rc;
    8.52 +          in Synchronized.change result (K res) end
    8.53 +          handle exn =>
    8.54 +            (Synchronized.change result (fn Wait => Signal | res => res); Exn.reraise exn)));
    8.55 +
    8.56 +    fun read_pid 0 = NONE
    8.57 +      | read_pid count =
    8.58 +          (case (Int.fromString (File.read pid_path) handle IO.Io _ => NONE) of
    8.59 +            NONE => (OS.Process.sleep (seconds 0.1); read_pid (count - 1))
    8.60 +          | some => some);
    8.61 +
    8.62 +    fun terminate NONE = ()
    8.63 +      | terminate (SOME pid) =
    8.64 +          let
    8.65 +            fun kill s =
    8.66 +              let
    8.67 +                val cmd = getenv_strict "CYGWIN_ROOT" ^ "\\bin\\bash.exe";
    8.68 +                val arg = "kill -" ^ s ^ " -" ^ string_of_int pid;
    8.69 +              in
    8.70 +                OS.Process.isSuccess (Windows.simpleExecute ("", quote cmd ^ " -c " ^ quote arg))
    8.71 +                  handle OS.SysErr _ => false
    8.72 +              end;
    8.73 +
    8.74 +            fun multi_kill count s =
    8.75 +              count = 0 orelse
    8.76 +                (kill s; kill "0") andalso
    8.77 +                (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s);
    8.78 +            val _ =
    8.79 +              multi_kill 10 "INT" andalso
    8.80 +              multi_kill 10 "TERM" andalso
    8.81 +              multi_kill 10 "KILL";
    8.82 +          in () end;
    8.83 +
    8.84 +    fun cleanup () =
    8.85 +     (Standard_Thread.interrupt_unsynchronized system_thread;
    8.86 +      cleanup_files ());
    8.87 +  in
    8.88 +    let
    8.89 +      val _ =
    8.90 +        restore_attributes (fn () =>
    8.91 +          Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) ();
    8.92 +
    8.93 +      val out = the_default "" (try File.read out_path);
    8.94 +      val err = the_default "" (try File.read err_path);
    8.95 +      val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc);
    8.96 +      val pid = read_pid 1;
    8.97 +      val _ = cleanup ();
    8.98 +    in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end
    8.99 +    handle exn => (terminate (read_pid 10); cleanup (); Exn.reraise exn)
   8.100 +  end);
   8.101 +
   8.102 +end;
     9.1 --- a/src/Pure/build-jars	Wed Mar 09 21:01:22 2016 +0100
     9.2 +++ b/src/Pure/build-jars	Thu Mar 10 09:50:53 2016 +0100
     9.3 @@ -9,7 +9,6 @@
     9.4  ## sources
     9.5  
     9.6  declare -a SOURCES=(
     9.7 -  Concurrent/bash.scala
     9.8    Concurrent/consumer_thread.scala
     9.9    Concurrent/counter.scala
    9.10    Concurrent/event_timer.scala
    9.11 @@ -74,6 +73,7 @@
    9.12    PIDE/xml.scala
    9.13    PIDE/yxml.scala
    9.14    ROOT.scala
    9.15 +  System/bash.scala
    9.16    System/command_line.scala
    9.17    System/cygwin.scala
    9.18    System/getopts.scala