# 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 *)