equal
deleted
inserted
replaced
36 try File.rm err_path; |
36 try File.rm err_path; |
37 try File.rm pid_path); |
37 try File.rm pid_path); |
38 val _ = cleanup_files (); |
38 val _ = cleanup_files (); |
39 |
39 |
40 val system_thread = |
40 val system_thread = |
41 Standard_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () => |
41 Isabelle_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () => |
42 Thread_Attributes.with_attributes Thread_Attributes.private_interrupts (fn _ => |
42 Thread_Attributes.with_attributes Thread_Attributes.private_interrupts (fn _ => |
43 let |
43 let |
44 val _ = File.write script_path script; |
44 val _ = File.write script_path script; |
45 val bash_script = |
45 val bash_script = |
46 "bash " ^ File.bash_path script_path ^ |
46 "bash " ^ File.bash_path script_path ^ |
84 multi_kill 10 "TERM" andalso |
84 multi_kill 10 "TERM" andalso |
85 multi_kill 10 "KILL"; |
85 multi_kill 10 "KILL"; |
86 in () end; |
86 in () end; |
87 |
87 |
88 fun cleanup () = |
88 fun cleanup () = |
89 (Standard_Thread.interrupt_unsynchronized system_thread; |
89 (Isabelle_Thread.interrupt_unsynchronized system_thread; |
90 cleanup_files ()); |
90 cleanup_files ()); |
91 in |
91 in |
92 let |
92 let |
93 val _ = |
93 val _ = |
94 restore_attributes (fn () => |
94 restore_attributes (fn () => |
130 try File.rm err_path; |
130 try File.rm err_path; |
131 try File.rm pid_path); |
131 try File.rm pid_path); |
132 val _ = cleanup_files (); |
132 val _ = cleanup_files (); |
133 |
133 |
134 val system_thread = |
134 val system_thread = |
135 Standard_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () => |
135 Isabelle_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () => |
136 Thread_Attributes.with_attributes Thread_Attributes.private_interrupts (fn _ => |
136 Thread_Attributes.with_attributes Thread_Attributes.private_interrupts (fn _ => |
137 let |
137 let |
138 val _ = File.write script_path script; |
138 val _ = File.write script_path script; |
139 val _ = getenv_strict "ISABELLE_BASH_PROCESS"; |
139 val _ = getenv_strict "ISABELLE_BASH_PROCESS"; |
140 val status = |
140 val status = |
180 multi_kill 10 Posix.Signal.term andalso |
180 multi_kill 10 Posix.Signal.term andalso |
181 multi_kill 10 Posix.Signal.kill; |
181 multi_kill 10 Posix.Signal.kill; |
182 in () end; |
182 in () end; |
183 |
183 |
184 fun cleanup () = |
184 fun cleanup () = |
185 (Standard_Thread.interrupt_unsynchronized system_thread; |
185 (Isabelle_Thread.interrupt_unsynchronized system_thread; |
186 cleanup_files ()); |
186 cleanup_files ()); |
187 in |
187 in |
188 let |
188 let |
189 val _ = |
189 val _ = |
190 restore_attributes (fn () => |
190 restore_attributes (fn () => |