# HG changeset patch
# User wenzelm
# Date 1185717603 -7200
# Node ID 0eacec17e8e756ab5027620101f1cb7e1e3c4276
# Parent  af1dd276fae085c5af5fae5c9ed05627ad9b740e
removed obsolete TOPLEVEL_ERROR etc. (cf. toplevel.ML);

diff -r af1dd276fae0 -r 0eacec17e8e7 src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Sun Jul 29 16:00:02 2007 +0200
+++ b/src/Pure/General/output.ML	Sun Jul 29 16:00:03 2007 +0200
@@ -44,10 +44,6 @@
   val debug_fn: (output -> unit) ref
   val debugging: bool ref
   val no_warnings: ('a -> 'b) -> 'a -> 'b
-  exception TOPLEVEL_ERROR
-  val do_toplevel_errors: bool ref
-  val toplevel_errors: ('a -> 'b) -> 'a -> 'b
-  val ML_errors: ('a -> 'b) -> 'a -> 'b
   val debug: (unit -> string) -> unit
   val error_msg: string -> unit
   val ml_output: (string -> unit) * (string -> unit)
@@ -124,20 +120,6 @@
 val ml_output = (writeln, error_msg);
 
 
-(* toplevel errors *)
-
-exception TOPLEVEL_ERROR;
-
-val do_toplevel_errors = ref true;
-
-fun toplevel_errors f x =
-  if ! do_toplevel_errors then
-    f x handle ERROR msg => (error_msg msg; raise TOPLEVEL_ERROR)
-  else f x;
-
-fun ML_errors f = setmp do_toplevel_errors true (toplevel_errors f);
-
-
 
 (** timing **)