equal
deleted
inserted
replaced
134 (fn () => |
134 (fn () => |
135 let |
135 let |
136 val task = the (Future.worker_task ()); |
136 val task = the (Future.worker_task ()); |
137 val _ = status task [Isabelle_Markup.running]; |
137 val _ = status task [Isabelle_Markup.running]; |
138 val result = Exn.capture (Future.interruptible_task e) (); |
138 val result = Exn.capture (Future.interruptible_task e) (); |
|
139 val _ = status task [Isabelle_Markup.finished, Isabelle_Markup.joined]; |
139 val _ = |
140 val _ = |
140 status task |
141 if is_some (Exn.get_res result) then () |
141 ([Isabelle_Markup.finished, Isabelle_Markup.joined] @ |
142 else |
142 (if is_some (Exn.get_res result) then [] else [Isabelle_Markup.failed])); |
143 (status task [Isabelle_Markup.failed]; |
|
144 Output.report (Markup.markup_only Isabelle_Markup.bad)); |
143 in Exn.release result end); |
145 in Exn.release result end); |
144 val _ = status (Future.task_of future) [Isabelle_Markup.forked]; |
146 val _ = status (Future.task_of future) [Isabelle_Markup.forked]; |
145 in future end) (); |
147 in future end) (); |
146 |
148 |
147 fun fork e = fork_name "Goal.fork" e; |
149 fun fork e = fork_name "Goal.fork" e; |