# HG changeset patch # User wenzelm # Date 1257891320 -3600 # Node ID 3713a5208671be91c28c9808edbd544972a8248d # Parent d25e6bd6ca95f35f1b348318dbf0225bbab452f8 generalized Runtime.toplevel_error wrt. output function; diff -r d25e6bd6ca95 -r 3713a5208671 src/Pure/Isar/runtime.ML --- a/src/Pure/Isar/runtime.ML Tue Nov 10 23:15:15 2009 +0100 +++ b/src/Pure/Isar/runtime.ML Tue Nov 10 23:15:20 2009 +0100 @@ -14,7 +14,7 @@ val exn_message: (exn -> Position.T) -> exn -> string val debugging: ('a -> 'b) -> 'a -> 'b val controlled_execution: ('a -> 'b) -> 'a -> 'b - val toplevel_error: (exn -> string) -> ('a -> 'b) -> 'a -> 'b + val toplevel_error: (exn -> unit) -> ('a -> 'b) -> 'a -> 'b end; structure Runtime: RUNTIME = @@ -96,12 +96,9 @@ |> debugging |> Future.interruptible_task; -fun toplevel_error exn_message f x = - let val ctxt = Option.map Context.proof_of (Context.thread_data ()) in - f x handle exn => - (Output.error_msg (exn_message (exn_context ctxt exn)); - raise TOPLEVEL_ERROR) - end; +fun toplevel_error output_exn f x = + let val ctxt = Option.map Context.proof_of (Context.thread_data ()) + in f x handle exn => (output_exn (exn_context ctxt exn); raise TOPLEVEL_ERROR) end; end; diff -r d25e6bd6ca95 -r 3713a5208671 src/Pure/ML/ml_compiler_polyml-5.3.ML --- a/src/Pure/ML/ml_compiler_polyml-5.3.ML Tue Nov 10 23:15:15 2009 +0100 +++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML Tue Nov 10 23:15:20 2009 +0100 @@ -154,7 +154,10 @@ (case phase2 of NONE => err "Static Errors" | SOME code => - apply_result ((code |> Runtime.debugging |> Runtime.toplevel_error exn_message) ()))); + apply_result + ((code + |> Runtime.debugging + |> Runtime.toplevel_error (Output.error_msg o exn_message)) ()))); (* compiler invocation *)