src/Pure/Isar/runtime.ML
changeset 45197 b6c527c64789
parent 44295 e43f0ea90c9a
child 45486 600682331b79
equal deleted inserted replaced
45196:78478d938cb8 45197:b6c527c64789
   124 fun toplevel_error output_exn f x = f x
   124 fun toplevel_error output_exn f x = f x
   125   handle exn =>
   125   handle exn =>
   126     if Exn.is_interrupt exn then reraise exn
   126     if Exn.is_interrupt exn then reraise exn
   127     else
   127     else
   128       let
   128       let
   129         val ctxt = Option.map Context.proof_of (Context.thread_data ());
   129         val opt_ctxt =
   130         val _ = output_exn (exn_context ctxt exn);
   130           (case Context.thread_data () of
       
   131             NONE => NONE
       
   132           | SOME context => try Context.proof_of context);
       
   133         val _ = output_exn (exn_context opt_ctxt exn);
   131       in raise TOPLEVEL_ERROR end;
   134       in raise TOPLEVEL_ERROR end;
   132 
   135 
   133 end;
   136 end;
   134 
   137