changeset 28463 | b8f16c92122a |
parent 28458 | 0966ac3f4a40 |
child 28553 | 675270d2d304 |
28462:6ec603695aaf | 28463:b8f16c92122a |
---|---|
307 |> debugging |
307 |> debugging |
308 |> interruptible; |
308 |> interruptible; |
309 |
309 |
310 fun program f = |
310 fun program f = |
311 (f |
311 (f |
312 |> debugging |
312 |> controlled_execution |
313 |> toplevel_error) (); |
313 |> toplevel_error) (); |
314 |
314 |
315 end; |
315 end; |
316 |
316 |
317 |
317 |