equal
deleted
inserted
replaced
172 Exn.capture (fn () => |
172 Exn.capture (fn () => |
173 (case result of |
173 (case result of |
174 Exn.Exn exn => |
174 Exn.Exn exn => |
175 (status task [Markup.failed]; |
175 (status task [Markup.failed]; |
176 status task [Markup.finished]; |
176 status task [Markup.finished]; |
177 Output.report [Markup.markup_only (Markup.bad ())]; |
177 Position.report pos (Markup.bad ()); |
178 if exec_id = 0 then () |
178 if exec_id = 0 then () |
179 else List.app (Future.error_message pos) (Runtime.exn_messages exn)) |
179 else List.app (Future.error_message pos) (Runtime.exn_messages exn)) |
180 | Exn.Res _ => |
180 | Exn.Res _ => |
181 status task [Markup.finished])) (); |
181 status task [Markup.finished])) (); |
182 val _ = status task [Markup.joined]; |
182 val _ = status task [Markup.joined]; |