equal
deleted
inserted
replaced
87 in Output.status (implode (map (Markup.markup_only o Markup.properties props) markups)) end; |
87 in Output.status (implode (map (Markup.markup_only o Markup.properties props) markups)) end; |
88 |
88 |
89 type params = {name: string, pos: Position.T, pri: int}; |
89 type params = {name: string, pos: Position.T, pri: int}; |
90 |
90 |
91 fun fork ({name, pos, pri}: params) e = |
91 fun fork ({name, pos, pri}: params) e = |
92 Multithreading.uninterruptible (fn _ => Position.setmp_thread_data pos (fn () => |
92 Thread_Attributes.uninterruptible (fn _ => Position.setmp_thread_data pos (fn () => |
93 let |
93 let |
94 val exec_id = the_default 0 (Position.parse_id pos); |
94 val exec_id = the_default 0 (Position.parse_id pos); |
95 val group = Future.worker_subgroup (); |
95 val group = Future.worker_subgroup (); |
96 val _ = change_state (apsnd (fn execs => |
96 val _ = change_state (apsnd (fn execs => |
97 (case Inttab.lookup execs exec_id of |
97 (case Inttab.lookup execs exec_id of |