31 val assert_all: ('a -> bool) -> 'a list -> ('a -> string) -> unit |
31 val assert_all: ('a -> bool) -> 'a list -> ('a -> string) -> unit |
32 val overwrite_warn: (''a * 'b) list * (''a * 'b) -> string -> (''a * 'b) list |
32 val overwrite_warn: (''a * 'b) list * (''a * 'b) -> string -> (''a * 'b) list |
33 datatype 'a error = Error of string | OK of 'a |
33 datatype 'a error = Error of string | OK of 'a |
34 val get_error: 'a error -> string option |
34 val get_error: 'a error -> string option |
35 val get_ok: 'a error -> 'a option |
35 val get_ok: 'a error -> 'a option |
36 datatype 'a result = Result of 'a | Exn of exn |
|
37 val get_result: 'a result -> 'a option |
|
38 val get_exn: 'a result -> exn option |
|
39 val handle_error: ('a -> 'b) -> 'a -> 'b error |
36 val handle_error: ('a -> 'b) -> 'a -> 'b error |
40 exception ERROR_MESSAGE of string |
37 exception ERROR_MESSAGE of string |
41 val transform_error: ('a -> 'b) -> 'a -> 'b |
38 val transform_error: ('a -> 'b) -> 'a -> 'b |
42 val transform_failure: (exn -> exn) -> ('a -> 'b) -> 'a -> 'b |
39 val transform_failure: (exn -> exn) -> ('a -> 'b) -> 'a -> 'b |
|
40 val timing: bool ref |
43 val cond_timeit: bool -> (unit -> 'a) -> 'a |
41 val cond_timeit: bool -> (unit -> 'a) -> 'a |
44 val timeit: (unit -> 'a) -> 'a |
42 val timeit: (unit -> 'a) -> 'a |
45 val timeap: ('a -> 'b) -> 'a -> 'b |
43 val timeap: ('a -> 'b) -> 'a -> 'b |
46 val timeap_msg: string -> ('a -> 'b) -> 'a -> 'b |
44 val timeap_msg: string -> ('a -> 'b) -> 'a -> 'b |
47 val timing: bool ref |
|
48 end; |
45 end; |
49 |
46 |
50 signature OUTPUT = |
47 signature OUTPUT = |
51 sig |
48 sig |
52 include BASIC_OUTPUT |
49 include BASIC_OUTPUT |
149 | get_error _ = None; |
146 | get_error _ = None; |
150 |
147 |
151 fun get_ok (OK x) = Some x |
148 fun get_ok (OK x) = Some x |
152 | get_ok _ = None; |
149 | get_ok _ = None; |
153 |
150 |
154 datatype 'a result = |
|
155 Result of 'a | |
|
156 Exn of exn; |
|
157 |
|
158 fun get_result (Result x) = Some x |
|
159 | get_result _ = None; |
|
160 |
|
161 fun get_exn (Exn exn) = Some exn |
|
162 | get_exn _ = None; |
|
163 |
|
164 fun handle_error f x = |
151 fun handle_error f x = |
165 let |
152 let |
166 val buffer = ref ([]: string list); |
153 val buffer = ref ([]: string list); |
167 fun capture s = buffer := ! buffer @ [s]; |
154 fun store_msg s = buffer := ! buffer @ [s]; |
168 fun err_msg () = if not (null (! buffer)) then error_msg (cat_lines (! buffer)) else (); |
155 fun err_msg () = if not (null (! buffer)) then error_msg (cat_lines (! buffer)) else (); |
169 in |
156 in |
170 (case Result (setmp error_fn capture f x) handle exn => Exn exn of |
157 (case Result (setmp error_fn store_msg f x) handle exn => Exn exn of |
171 Result y => (err_msg (); OK y) |
158 Result y => (err_msg (); OK y) |
172 | Exn ERROR => Error (cat_lines (! buffer)) |
159 | Exn ERROR => Error (cat_lines (! buffer)) |
173 | Exn exn => (err_msg (); raise exn)) |
160 | Exn exn => (err_msg (); raise exn)) |
174 end; |
161 end; |
175 |
162 |
190 transform_error f x handle Interrupt => raise Interrupt | e => raise exn e; |
177 transform_error f x handle Interrupt => raise Interrupt | e => raise exn e; |
191 |
178 |
192 |
179 |
193 |
180 |
194 (** timing **) |
181 (** timing **) |
|
182 |
|
183 (*global timing mode*) |
|
184 val timing = ref false; |
195 |
185 |
196 (*a conditional timing function: applies f to () and, if the flag is true, |
186 (*a conditional timing function: applies f to () and, if the flag is true, |
197 prints its runtime on warning channel*) |
187 prints its runtime on warning channel*) |
198 fun cond_timeit flag f = |
188 fun cond_timeit flag f = |
199 if flag then |
189 if flag then |
207 |
197 |
208 (*timed application function*) |
198 (*timed application function*) |
209 fun timeap f x = timeit (fn () => f x); |
199 fun timeap f x = timeit (fn () => f x); |
210 fun timeap_msg s f x = (warning s; timeap f x); |
200 fun timeap_msg s f x = (warning s; timeap f x); |
211 |
201 |
212 (*global timing mode*) |
|
213 val timing = ref false; |
|
214 |
|
215 end; |
202 end; |
216 |
203 |
217 structure BasicOutput: BASIC_OUTPUT = Output; |
204 structure BasicOutput: BASIC_OUTPUT = Output; |
218 open BasicOutput; |
205 open BasicOutput; |