src/Pure/Isar/runtime.ML
changeset 59056 cbe9563c03d1
parent 59055 5a7157b8e870
child 59058 a78612c67ec0
--- a/src/Pure/Isar/runtime.ML	Wed Nov 26 14:35:55 2014 +0100
+++ b/src/Pure/Isar/runtime.ML	Wed Nov 26 15:44:32 2014 +0100
@@ -17,6 +17,7 @@
   val exn_error_message: exn -> unit
   val exn_system_message: exn -> unit
   val exn_trace: (unit -> 'a) -> 'a
+  val exn_trace_system: (unit -> 'a) -> 'a
   val debugging: Context.generic option -> ('a -> 'b) -> 'a -> 'b
   val controlled_execution: Context.generic option -> ('a -> 'b) -> 'a -> 'b
   val toplevel_error: (exn -> unit) -> ('a -> 'b) -> 'a -> 'b
@@ -134,6 +135,7 @@
 val exn_error_message = Output.error_message o exn_message;
 val exn_system_message = Output.system_message o exn_message;
 fun exn_trace e = print_exception_trace exn_message tracing e;
+fun exn_trace_system e = print_exception_trace exn_message Output.system_message e;