equal
deleted
inserted
replaced
109 |
109 |
110 |
110 |
111 (** controlled execution **) |
111 (** controlled execution **) |
112 |
112 |
113 fun debugging f x = |
113 fun debugging f x = |
114 if ! debug then |
114 if ! debug |
115 Exn.release (exception_trace (fn () => |
115 then exception_trace (fn () => f x) |
116 Exn.Res (f x) handle |
|
117 exn as UNDEF => Exn.Exn exn |
|
118 | exn as EXCURSION_FAIL _ => Exn.Exn exn)) |
|
119 else f x; |
116 else f x; |
120 |
117 |
121 fun controlled_execution f x = |
118 fun controlled_execution f x = |
122 (f |> debugging |> Future.interruptible_task) x; |
119 (f |> debugging |> Future.interruptible_task) x; |
123 |
120 |