1.1 --- a/src/Pure/Concurrent/bash.ML	Thu Nov 28 13:59:00 2013 +0100
     1.2 +++ b/src/Pure/Concurrent/bash.ML	Sat Nov 30 15:05:10 2013 +0100
     1.3 @@ -23,6 +23,13 @@
     1.4      val err_path = File.tmp_path (Path.basic ("bash_err" ^ id));
     1.5      val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id));
     1.6  
     1.7 +    fun cleanup_files () =
     1.8 +     (try File.rm script_path;
     1.9 +      try File.rm out_path;
    1.10 +      try File.rm err_path;
    1.11 +      try File.rm pid_path);
    1.12 +    val _ = cleanup_files ();
    1.13 +
    1.14      val system_thread =
    1.15        Simple_Thread.fork false (fn () =>
    1.16          Multithreading.with_attributes Multithreading.private_interrupts (fn _ =>
    1.17 @@ -55,37 +62,36 @@
    1.18            handle exn =>
    1.19              (Synchronized.change result (fn Wait => Signal | res => res); reraise exn)));
    1.20  
    1.21 -    fun get_pid () = Int.fromString (File.read pid_path) handle IO.Io _ => NONE;
    1.22 +    fun read_pid 0 = NONE
    1.23 +      | read_pid count =
    1.24 +          (case (Int.fromString (File.read pid_path) handle IO.Io _ => NONE) of
    1.25 +            NONE => (OS.Process.sleep (seconds 0.1); read_pid (count - 1))
    1.26 +          | some => some);
    1.27  
    1.28 -    fun terminate opt_pid =
    1.29 -      let
    1.30 -        val sig_test = Posix.Signal.fromWord 0w0;
    1.31 +    fun terminate NONE = ()
    1.32 +      | terminate (SOME pid) =
    1.33 +          let
    1.34 +            val sig_test = Posix.Signal.fromWord 0w0;
    1.35  
    1.36 -        fun kill_group pid s =
    1.37 -          (Posix.Process.kill
    1.38 -            (Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid)), s); true)
    1.39 -          handle OS.SysErr _ => false;
    1.40 +            fun kill_group pid s =
    1.41 +              (Posix.Process.kill
    1.42 +                (Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid)), s); true)
    1.43 +              handle OS.SysErr _ => false;
    1.44  
    1.45 -        fun kill s =
    1.46 -          (case opt_pid of
    1.47 -            NONE => true
    1.48 -          | SOME pid => (kill_group pid s; kill_group pid sig_test));
    1.49 +            fun kill s = (kill_group pid s; kill_group pid sig_test);
    1.50  
    1.51 -        fun multi_kill count s =
    1.52 -          count = 0 orelse
    1.53 -            kill s andalso (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s);
    1.54 -        val _ =
    1.55 -          multi_kill 10 Posix.Signal.int andalso
    1.56 -          multi_kill 10 Posix.Signal.term andalso
    1.57 -          multi_kill 10 Posix.Signal.kill;
    1.58 -      in () end;
    1.59 +            fun multi_kill count s =
    1.60 +              count = 0 orelse
    1.61 +                kill s andalso (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s);
    1.62 +            val _ =
    1.63 +              multi_kill 10 Posix.Signal.int andalso
    1.64 +              multi_kill 10 Posix.Signal.term andalso
    1.65 +              multi_kill 10 Posix.Signal.kill;
    1.66 +          in () end;
    1.67  
    1.68      fun cleanup () =
    1.69       (Simple_Thread.interrupt_unsynchronized system_thread;
    1.70 -      try File.rm script_path;
    1.71 -      try File.rm out_path;
    1.72 -      try File.rm err_path;
    1.73 -      try File.rm pid_path);
    1.74 +      cleanup_files ());
    1.75    in
    1.76      let
    1.77        val _ =
    1.78 @@ -95,10 +101,10 @@
    1.79        val out = the_default "" (try File.read out_path);
    1.80        val err = the_default "" (try File.read err_path);
    1.81        val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc);
    1.82 -      val pid = get_pid ();
    1.83 +      val pid = read_pid 1;
    1.84        val _ = cleanup ();
    1.85      in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end
    1.86 -    handle exn => (terminate (get_pid ()); cleanup (); reraise exn)
    1.87 +    handle exn => (terminate (read_pid 10); cleanup (); reraise exn)
    1.88    end);
    1.89  
    1.90  end;