fixed handle_error: cat_lines;
authorwenzelm
Tue May 19 17:15:30 1998 +0200 (1998-05-19)
changeset 4945d8c809afafb8
parent 4944 a6e71e5a1004
child 4946 d8e5c6e31854
fixed handle_error: cat_lines;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Tue May 19 17:15:04 1998 +0200
     1.2 +++ b/src/Pure/library.ML	Tue May 19 17:15:30 1998 +0200
     1.3 @@ -1053,12 +1053,12 @@
     1.4  
     1.5  fun handle_error f x =
     1.6    let
     1.7 -    val buffer = ref "";
     1.8 -    fun capture s = buffer := ! buffer ^ s ^ "\n";
     1.9 +    val buffer = ref ([]: string list);
    1.10 +    fun capture s = buffer := ! buffer @ [s];
    1.11      val result = Some (setmp error_fn capture f x) handle ERROR => None;
    1.12    in
    1.13      (case result of
    1.14 -      None => Error (! buffer)
    1.15 +      None => Error (cat_lines (! buffer))
    1.16      | Some y => OK y)
    1.17    end;
    1.18