author | wenzelm |
Tue, 19 May 1998 17:15:30 +0200 | |
changeset 4945 | d8c809afafb8 |
parent 4944 | a6e71e5a1004 |
child 4946 | d8e5c6e31854 |
--- a/src/Pure/library.ML Tue May 19 17:15:04 1998 +0200 +++ b/src/Pure/library.ML Tue May 19 17:15:30 1998 +0200 @@ -1053,12 +1053,12 @@ fun handle_error f x = let - val buffer = ref ""; - fun capture s = buffer := ! buffer ^ s ^ "\n"; + val buffer = ref ([]: string list); + fun capture s = buffer := ! buffer @ [s]; val result = Some (setmp error_fn capture f x) handle ERROR => None; in (case result of - None => Error (! buffer) + None => Error (cat_lines (! buffer)) | Some y => OK y) end;