equal
deleted
inserted
replaced
12 if ML_System.platform_is_windows then ML |
12 if ML_System.platform_is_windows then ML |
13 \<open> |
13 \<open> |
14 structure Bash: BASH = |
14 structure Bash: BASH = |
15 struct |
15 struct |
16 |
16 |
17 val process = Multithreading.uninterruptible (fn restore_attributes => fn script => |
17 val process = Thread_Attributes.uninterruptible (fn restore_attributes => fn script => |
18 let |
18 let |
19 datatype result = Wait | Signal | Result of int; |
19 datatype result = Wait | Signal | Result of int; |
20 val result = Synchronized.var "bash_result" Wait; |
20 val result = Synchronized.var "bash_result" Wait; |
21 |
21 |
22 val id = serial_string (); |
22 val id = serial_string (); |
32 try File.rm pid_path); |
32 try File.rm pid_path); |
33 val _ = cleanup_files (); |
33 val _ = cleanup_files (); |
34 |
34 |
35 val system_thread = |
35 val system_thread = |
36 Standard_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () => |
36 Standard_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () => |
37 Multithreading.with_attributes Multithreading.private_interrupts (fn _ => |
37 Thread_Attributes.with_attributes Thread_Attributes.private_interrupts (fn _ => |
38 let |
38 let |
39 val _ = File.write script_path script; |
39 val _ = File.write script_path script; |
40 val bash_script = |
40 val bash_script = |
41 "bash " ^ File.bash_path script_path ^ |
41 "bash " ^ File.bash_path script_path ^ |
42 " > " ^ File.bash_path out_path ^ |
42 " > " ^ File.bash_path out_path ^ |
103 else ML |
103 else ML |
104 \<open> |
104 \<open> |
105 structure Bash: BASH = |
105 structure Bash: BASH = |
106 struct |
106 struct |
107 |
107 |
108 val process = Multithreading.uninterruptible (fn restore_attributes => fn script => |
108 val process = Thread_Attributes.uninterruptible (fn restore_attributes => fn script => |
109 let |
109 let |
110 datatype result = Wait | Signal | Result of int; |
110 datatype result = Wait | Signal | Result of int; |
111 val result = Synchronized.var "bash_result" Wait; |
111 val result = Synchronized.var "bash_result" Wait; |
112 |
112 |
113 val id = serial_string (); |
113 val id = serial_string (); |
123 try File.rm pid_path); |
123 try File.rm pid_path); |
124 val _ = cleanup_files (); |
124 val _ = cleanup_files (); |
125 |
125 |
126 val system_thread = |
126 val system_thread = |
127 Standard_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () => |
127 Standard_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () => |
128 Multithreading.with_attributes Multithreading.private_interrupts (fn _ => |
128 Thread_Attributes.with_attributes Thread_Attributes.private_interrupts (fn _ => |
129 let |
129 let |
130 val _ = File.write script_path script; |
130 val _ = File.write script_path script; |
131 val _ = getenv_strict "ISABELLE_BASH_PROCESS"; |
131 val _ = getenv_strict "ISABELLE_BASH_PROCESS"; |
132 val status = |
132 val status = |
133 OS.Process.system |
133 OS.Process.system |