429 nodes_of (the_version state version_id) |> String_Graph.schedule |
429 nodes_of (the_version state version_id) |> String_Graph.schedule |
430 (fn deps => fn (name, node) => |
430 (fn deps => fn (name, node) => |
431 if visible_node node orelse pending_result node then |
431 if visible_node node orelse pending_result node then |
432 let |
432 let |
433 fun body () = |
433 fun body () = |
434 if forall finished_import deps then |
434 (if forall finished_import deps then |
435 iterate_entries (fn (_, opt_exec) => fn () => |
435 iterate_entries (fn (_, opt_exec) => fn () => |
436 (case opt_exec of |
436 (case opt_exec of |
437 SOME exec => |
437 SOME exec => |
438 if Execution.is_running execution_id |
438 if Execution.is_running execution_id |
439 then SOME (Command.exec execution_id exec) |
439 then SOME (Command.exec execution_id exec) |
440 else NONE |
440 else NONE |
441 | NONE => NONE)) node () |
441 | NONE => NONE)) node () |
442 else (); |
442 else ()) |
|
443 handle exn => (Output.system_message (Runtime.exn_message exn); reraise exn); |
443 val future = |
444 val future = |
444 (singleton o Future.forks) |
445 (singleton o Future.forks) |
445 {name = "theory:" ^ name, |
446 {name = "theory:" ^ name, |
446 group = SOME (Future.new_group NONE), |
447 group = SOME (Future.new_group NONE), |
447 deps = Future.task_of delay_request' :: maps (the_list o #2 o #2) deps, |
448 deps = Future.task_of delay_request' :: maps (the_list o #2 o #2) deps, |