src/Pure/Isar/runtime.ML
changeset 42595 22f8c2483bd2
parent 40575 035b2afbeb2e
child 43107 578a51fae383
     1.1 --- a/src/Pure/Isar/runtime.ML	Tue Feb 08 14:28:15 2011 +0100
     1.2 +++ b/src/Pure/Isar/runtime.ML	Tue Feb 08 16:11:52 2011 +0100
     1.3 @@ -106,10 +106,8 @@
     1.4        | exn as EXCURSION_FAIL _ => Exn.Exn exn))
     1.5    else f x;
     1.6  
     1.7 -fun controlled_execution f =
     1.8 -  f
     1.9 -  |> debugging
    1.10 -  |> Future.interruptible_task;
    1.11 +fun controlled_execution f x =
    1.12 +  ((f |> debugging |> Future.interruptible_task) x before Multithreading.interrupted ());
    1.13  
    1.14  fun toplevel_error output_exn f x = f x
    1.15    handle exn =>