# HG changeset patch
# User wenzelm
# Date 1185212747 -7200
# Node ID f2181804fced039b2fc33cb98d2d721a9d3ca624
# Parent  e543359fe8b60c61c53e7e23b48f71909ed3e6bb
marked some CRITICAL sections;
eliminated transform_failure (to avoid critical section for main transactions);
removed unused exceptions MetaSimplifier.SIMPROC_FAIL, Attrib.ATTRIB_FAIL, Method.METHOD_FAIL, Antiquote.ANTIQUOTE_FAIL;

diff -r e543359fe8b6 -r f2181804fced src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Mon Jul 23 19:45:46 2007 +0200
+++ b/src/Pure/Isar/toplevel.ML	Mon Jul 23 19:45:47 2007 +0200
@@ -261,11 +261,6 @@
   | exn_msg detailed (EXCURSION_FAIL (exn, msg)) = cat_lines [exn_msg detailed exn, msg]
   | exn_msg false (THEORY (msg, _)) = msg
   | exn_msg true (THEORY (msg, thys)) = raised "THEORY" (msg :: map Context.str_of_thy thys)
-  | exn_msg detailed (MetaSimplifier.SIMPROC_FAIL (name, exn)) =
-      fail_msg detailed "simproc" ((name, Position.none), exn)
-  | exn_msg detailed (Attrib.ATTRIB_FAIL info) = fail_msg detailed "attribute" info
-  | exn_msg detailed (Method.METHOD_FAIL info) = fail_msg detailed "method" info
-  | exn_msg detailed (Antiquote.ANTIQUOTE_FAIL info) = fail_msg detailed "antiquotation" info
   | exn_msg false (Syntax.AST (msg, _)) = raised "AST" [msg]
   | exn_msg true (Syntax.AST (msg, asts)) =
       raised "AST" (msg :: map (Pretty.string_of o Syntax.pretty_ast) asts)
@@ -283,9 +278,7 @@
   | exn_msg _ Empty = raised "Empty" []
   | exn_msg _ Subscript = raised "Subscript" []
   | exn_msg _ (Fail msg) = raised "Fail" [msg]
-  | exn_msg _ exn = General.exnMessage exn
-and fail_msg detailed kind ((name, pos), exn) =
-  "Error in " ^ kind ^ " " ^ quote name ^ Position.str_of pos ^ ":\n" ^ exn_msg detailed exn;
+  | exn_msg _ exn = General.exnMessage exn;
 
 in
 
@@ -302,9 +295,7 @@
 local
 
 fun debugging f x =
-  if ! debug then
-    setmp Library.do_transform_failure false
-      exception_trace (fn () => f x)
+  if ! debug then exception_trace (fn () => f x)
   else f x;
 
 fun interruptible f x =
@@ -721,13 +712,13 @@
 
 nonfix >> >>>;
 
-fun >> tr =
+fun >> tr = CRITICAL (fn () =>
   (case apply true tr (get_state ()) of
     NONE => false
   | SOME (state', exn_info) =>
       (global_state := (state', exn_info);
         print_exn exn_info;
-        true));
+        true)));
 
 fun >>> [] = ()
   | >>> (tr :: trs) = if >> tr then >>> trs else ();