# HG changeset patch
# User wenzelm
# Date 1199379043 -3600
# Node ID decb98ff92dd581e6ef58b75953132087a49133a
# Parent  c7aaa3f6f0ac5d208ef85ea78b4b1ddfb59f44f6
toplevel print_exn: proper setmp_thread_properties;

diff -r c7aaa3f6f0ac -r decb98ff92dd src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Thu Jan 03 17:50:42 2008 +0100
+++ b/src/Pure/Isar/toplevel.ML	Thu Jan 03 17:50:43 2008 +0100
@@ -295,9 +295,7 @@
 in
 
 fun exn_message exn = exn_msg (! debug) exn;
-
-fun print_exn NONE = ()
-  | print_exn (SOME (exn, s)) = Output.error_msg (cat_lines [exn_message exn, s]);
+fun print_exn (exn, s) = Output.error_msg (cat_lines [exn_message exn, s]);
 
 end;
 
@@ -770,7 +768,9 @@
     NONE => false
   | SOME (state', exn_info) =>
       (global_state := (state', exn_info);
-        print_exn exn_info;
+        (case exn_info of
+          NONE => ()
+        | SOME err => setmp_thread_properties tr print_exn err);
         true));
 
 fun >>> [] = ()