55 Synchronized.timed_access v (K (SOME Time.zeroTime)) |
55 Synchronized.timed_access v (K (SOME Time.zeroTime)) |
56 (fn expr => |
56 (fn expr => |
57 (case expr of |
57 (case expr of |
58 Expr (exec_id, body) => |
58 Expr (exec_id, body) => |
59 uninterruptible (fn restore_attributes => fn () => |
59 uninterruptible (fn restore_attributes => fn () => |
60 if Execution.running execution_id exec_id [Future.the_worker_group ()] then |
60 let val group = Future.worker_subgroup () in |
61 let |
61 if Execution.running execution_id exec_id [group] then |
62 val res = |
62 let |
63 (body |
63 val res = |
64 |> restore_attributes |
64 (body |
65 |> Future.worker_nest "Command.memo_exec" |
65 |> restore_attributes |
66 |> Exn.interruptible_capture) (); |
66 |> Future.worker_context "Command.memo_exec" group |
67 in SOME ((), Result res) end |
67 |> Exn.interruptible_capture) (); |
68 else SOME ((), expr)) () |
68 in SOME ((), Result res) end |
|
69 else SOME ((), expr) |
|
70 end) () |
69 | Result _ => SOME ((), expr))) |
71 | Result _ => SOME ((), expr))) |
70 |> (fn NONE => error "Conflicting command execution" | _ => ()); |
72 |> (fn NONE => error "Conflicting command execution" | _ => ()); |
71 |
73 |
72 fun memo_fork params execution_id (Memo v) = |
74 fun memo_fork params execution_id (Memo v) = |
73 (case Synchronized.value v of |
75 (case Synchronized.value v of |