src/Tools/Code/code_runtime.ML
changeset 40235 87998864284e
parent 40150 1348d4982a17
child 40257 323f7aad54b0
     1.1 --- a/src/Tools/Code/code_runtime.ML	Thu Oct 28 21:59:01 2010 +0200
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Thu Oct 28 22:04:00 2010 +0200
     1.3 @@ -105,7 +105,7 @@
     1.4      val (program_code, [SOME value_name']) = serializer naming program' [value_name];
     1.5      val value_code = space_implode " "
     1.6        (value_name' :: "()" :: map (enclose "(" ")") args);
     1.7 -  in Exn.capture (value ctxt cookie) (program_code, value_code) end;
     1.8 +  in Exn.interruptible_capture (value ctxt cookie) (program_code, value_code) end;
     1.9  
    1.10  fun partiality_as_none e = SOME (Exn.release e)
    1.11    handle General.Match => NONE