# HG changeset patch # User wenzelm # Date 1310833202 -7200 # Node ID 529159f81d06d8c053e10a87c5d50eec216541cc # Parent e6226e100ac56457d91d503bbdd1f6fcc190c113 more general bash_process, which allows to terminate background processes as well; diff -r e6226e100ac5 -r 529159f81d06 src/Pure/Concurrent/bash.ML --- a/src/Pure/Concurrent/bash.ML Sat Jul 16 18:11:14 2011 +0200 +++ b/src/Pure/Concurrent/bash.ML Sat Jul 16 18:20:02 2011 +0200 @@ -4,7 +4,7 @@ GNU bash processes, with propagation of interrupts. *) -val bash_output = uninterruptible (fn restore_attributes => fn script => +val bash_process = uninterruptible (fn restore_attributes => fn script => let datatype result = Wait | Signal | Result of int; val result = Synchronized.var "bash_result" Wait; @@ -39,7 +39,9 @@ handle exn => (Synchronized.change result (fn Wait => Signal | res => res); reraise exn))); - fun terminate () = + fun get_pid () = Int.fromString (File.read pid_path) handle IO.Io _ => NONE; + + fun terminate opt_pid = let val sig_test = Posix.Signal.fromWord 0w0; @@ -49,10 +51,9 @@ handle OS.SysErr _ => false; fun kill s = - (case Int.fromString (File.read pid_path) of + (case opt_pid of NONE => true - | SOME pid => (kill_group pid s; kill_group pid sig_test)) - handle IO.Io _ => true; + | SOME pid => (kill_group pid s; kill_group pid sig_test)); fun multi_kill count s = count = 0 orelse @@ -76,8 +77,9 @@ val output = the_default "" (try File.read output_path); val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc); + val pid = get_pid (); val _ = cleanup (); - in (output, rc) end - handle exn => (terminate(); cleanup (); reraise exn) + in {output = output, rc = rc, terminate = fn () => terminate pid} end + handle exn => (terminate (get_pid ()); cleanup (); reraise exn) end); diff -r e6226e100ac5 -r 529159f81d06 src/Pure/Concurrent/bash_ops.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Concurrent/bash_ops.ML Sat Jul 16 18:20:02 2011 +0200 @@ -0,0 +1,15 @@ +(* Title: Pure/Concurrent/bash_ops.ML + Author: Makarius + +Derived operations for bash_process. +*) + +fun bash_output s = + let val {output, rc, ...} = bash_process s + in (output, rc) end; + +fun bash s = + (case bash_output s of + ("", rc) => rc + | (out, rc) => (writeln (perhaps (try (unsuffix "\n")) out); rc)); + diff -r e6226e100ac5 -r 529159f81d06 src/Pure/Concurrent/bash_sequential.ML --- a/src/Pure/Concurrent/bash_sequential.ML Sat Jul 16 18:11:14 2011 +0200 +++ b/src/Pure/Concurrent/bash_sequential.ML Sat Jul 16 18:20:02 2011 +0200 @@ -5,7 +5,7 @@ could work via the controlling tty). *) -fun bash_output script = +fun bash_process script = let val id = serial_string (); val script_path = File.tmp_path (Path.basic ("bash_script" ^ id)); @@ -28,7 +28,7 @@ val output = the_default "" (try File.read output_path); val _ = cleanup (); - in (output, rc) end + in {output = output, rc = rc, terminate = fn () => ()} end handle exn => (cleanup (); reraise exn) end; diff -r e6226e100ac5 -r 529159f81d06 src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Sat Jul 16 18:11:14 2011 +0200 +++ b/src/Pure/IsaMakefile Sat Jul 16 18:20:02 2011 +0200 @@ -53,6 +53,7 @@ $(OUT)/Pure: $(BOOTSTRAP_FILES) \ Concurrent/bash.ML \ + Concurrent/bash_ops.ML \ Concurrent/bash_sequential.ML \ Concurrent/cache.ML \ Concurrent/future.ML \ diff -r e6226e100ac5 -r 529159f81d06 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Sat Jul 16 18:11:14 2011 +0200 +++ b/src/Pure/ROOT.ML Sat Jul 16 18:20:02 2011 +0200 @@ -79,11 +79,7 @@ if Multithreading.available then use "Concurrent/bash.ML" else use "Concurrent/bash_sequential.ML"; - -fun bash s = - (case bash_output s of - ("", rc) => rc - | (out, rc) => (writeln (perhaps (try (unsuffix "\n")) out); rc)); +use "Concurrent/bash_ops.ML"; use "Concurrent/mailbox.ML"; use "Concurrent/task_queue.ML";