# HG changeset patch
# User wenzelm
# Date 1120489755 -7200
# Node ID f1ea17a4f22269112ddb9f8e036217eb92f59018
# Parent  154a84e1a4f78a0e4d89ff607e772d8806e1e023
added transform_exceptions: bool ref;

diff -r 154a84e1a4f7 -r f1ea17a4f222 src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Mon Jul 04 17:08:19 2005 +0200
+++ b/src/Pure/General/output.ML	Mon Jul 04 17:09:15 2005 +0200
@@ -68,6 +68,7 @@
   val raw: string -> string
   val add_mode: string ->
     (string -> string * real) * (string * int -> string) * (string -> string) -> unit
+  val transform_exceptions: bool ref
 end;
 
 structure Output: OUTPUT =
@@ -196,18 +197,24 @@
 
 (* transform ERROR into ERROR_MESSAGE *)
 
+val transform_exceptions = ref true;
+
 exception ERROR_MESSAGE of string;
 
 fun transform_error f x =
-  (case handle_error f x of
-    OK y => y
-  | Error msg => raise ERROR_MESSAGE msg);
+  if ! transform_exceptions then
+    (case handle_error f x of
+      OK y => y
+    | Error msg => raise ERROR_MESSAGE msg)
+  else f x;
 
 
 (* transform any exception, including ERROR *)
 
 fun transform_failure exn f x =
-  transform_error f x handle Interrupt => raise Interrupt | e => raise exn e;
+  if ! transform_exceptions then
+    transform_error f x handle Interrupt => raise Interrupt | e => raise exn e
+  else f x;