removed obsolete TOPLEVEL_ERROR etc. (cf. toplevel.ML);
authorwenzelm
Sun Jul 29 16:00:03 2007 +0200 (2007-07-29)
changeset 240540eacec17e8e7
parent 24053 af1dd276fae0
child 24055 f7483532537b
removed obsolete TOPLEVEL_ERROR etc. (cf. toplevel.ML);
src/Pure/General/output.ML
     1.1 --- a/src/Pure/General/output.ML	Sun Jul 29 16:00:02 2007 +0200
     1.2 +++ b/src/Pure/General/output.ML	Sun Jul 29 16:00:03 2007 +0200
     1.3 @@ -44,10 +44,6 @@
     1.4    val debug_fn: (output -> unit) ref
     1.5    val debugging: bool ref
     1.6    val no_warnings: ('a -> 'b) -> 'a -> 'b
     1.7 -  exception TOPLEVEL_ERROR
     1.8 -  val do_toplevel_errors: bool ref
     1.9 -  val toplevel_errors: ('a -> 'b) -> 'a -> 'b
    1.10 -  val ML_errors: ('a -> 'b) -> 'a -> 'b
    1.11    val debug: (unit -> string) -> unit
    1.12    val error_msg: string -> unit
    1.13    val ml_output: (string -> unit) * (string -> unit)
    1.14 @@ -124,20 +120,6 @@
    1.15  val ml_output = (writeln, error_msg);
    1.16  
    1.17  
    1.18 -(* toplevel errors *)
    1.19 -
    1.20 -exception TOPLEVEL_ERROR;
    1.21 -
    1.22 -val do_toplevel_errors = ref true;
    1.23 -
    1.24 -fun toplevel_errors f x =
    1.25 -  if ! do_toplevel_errors then
    1.26 -    f x handle ERROR msg => (error_msg msg; raise TOPLEVEL_ERROR)
    1.27 -  else f x;
    1.28 -
    1.29 -fun ML_errors f = setmp do_toplevel_errors true (toplevel_errors f);
    1.30 -
    1.31 -
    1.32  
    1.33  (** timing **)
    1.34