1.1 --- a/src/Pure/General/output.ML	Sat Jun 05 13:06:04 2004 +0200
     1.2 +++ b/src/Pure/General/output.ML	Sat Jun 05 13:06:28 2004 +0200
     1.3 @@ -33,18 +33,15 @@
     1.4    datatype 'a error = Error of string | OK of 'a
     1.5    val get_error: 'a error -> string option
     1.6    val get_ok: 'a error -> 'a option
     1.7 -  datatype 'a result = Result of 'a | Exn of exn
     1.8 -  val get_result: 'a result -> 'a option
     1.9 -  val get_exn: 'a result -> exn option
    1.10    val handle_error: ('a -> 'b) -> 'a -> 'b error
    1.11    exception ERROR_MESSAGE of string
    1.12    val transform_error: ('a -> 'b) -> 'a -> 'b
    1.13    val transform_failure: (exn -> exn) -> ('a -> 'b) -> 'a -> 'b
    1.14 +  val timing: bool ref
    1.15    val cond_timeit: bool -> (unit -> 'a) -> 'a
    1.16    val timeit: (unit -> 'a) -> 'a
    1.17    val timeap: ('a -> 'b) -> 'a -> 'b
    1.18    val timeap_msg: string -> ('a -> 'b) -> 'a -> 'b
    1.19 -  val timing: bool ref
    1.20  end;
    1.21  
    1.22  signature OUTPUT =
    1.23 @@ -151,23 +148,13 @@
    1.24  fun get_ok (OK x) = Some x
    1.25    | get_ok _ = None;
    1.26  
    1.27 -datatype 'a result =
    1.28 -  Result of 'a |
    1.29 -  Exn of exn;
    1.30 -
    1.31 -fun get_result (Result x) = Some x
    1.32 -  | get_result _ = None;
    1.33 -
    1.34 -fun get_exn (Exn exn) = Some exn
    1.35 -  | get_exn _ = None;
    1.36 -
    1.37  fun handle_error f x =
    1.38    let
    1.39      val buffer = ref ([]: string list);
    1.40 -    fun capture s = buffer := ! buffer @ [s];
    1.41 +    fun store_msg s = buffer := ! buffer @ [s];
    1.42      fun err_msg () = if not (null (! buffer)) then error_msg (cat_lines (! buffer)) else ();
    1.43    in
    1.44 -    (case Result (setmp error_fn capture f x) handle exn => Exn exn of
    1.45 +    (case Result (setmp error_fn store_msg f x) handle exn => Exn exn of
    1.46        Result y => (err_msg (); OK y)
    1.47      | Exn ERROR => Error (cat_lines (! buffer))
    1.48      | Exn exn => (err_msg (); raise exn))
    1.49 @@ -193,6 +180,9 @@
    1.50  
    1.51  (** timing **)
    1.52  
    1.53 +(*global timing mode*)
    1.54 +val timing = ref false;
    1.55 +
    1.56  (*a conditional timing function: applies f to () and, if the flag is true,
    1.57    prints its runtime on warning channel*)
    1.58  fun cond_timeit flag f =
    1.59 @@ -209,9 +199,6 @@
    1.60  fun timeap f x = timeit (fn () => f x);
    1.61  fun timeap_msg s f x = (warning s; timeap f x);
    1.62  
    1.63 -(*global timing mode*)
    1.64 -val timing = ref false;
    1.65 -
    1.66  end;
    1.67  
    1.68  structure BasicOutput: BASIC_OUTPUT = Output;