diff --git a/src/libraries/utils/command.ml b/src/libraries/utils/command.ml index 22ab26bbb6a8c694c5244c66eb5762068ce9e68d..f51fc989837ddab11a87371e7e2e41087e1e7b98 100644 --- a/src/libraries/utils/command.ml +++ b/src/libraries/utils/command.ml @@ -111,11 +111,13 @@ let print_file file job = (* -------------------------------------------------------------------------- *) type timer = float ref -type 'a result = Result of 'a | Error of exn +type 'a result = Result of 'a | Error of Printexc.raw_backtrace * exn let dt_max tm dt = match tm with Some r when dt > !r -> r := dt | _ -> () let dt_add tm dt = match tm with Some r -> r := !r +. dt | _ -> () -let return = function Result x -> x | Error e -> raise e -let catch f x = try Result(f x) with e -> Error e +let return = function Result x -> x | Error (bt,e) -> Printexc.raise_with_backtrace e bt +let catch f x = try Result(f x) with e -> + let bt = Printexc.get_raw_backtrace () in + Error (bt,e) let time ?rmax ?radd job data = begin let t0 = Sys.time () in diff --git a/src/libraries/utils/command.mli b/src/libraries/utils/command.mli index 0643c00007d54479b2fbf20d7b197be26bb72232..10449cbf13070bd6ab7cd015289eda2c8bfb80db 100644 --- a/src/libraries/utils/command.mli +++ b/src/libraries/utils/command.mli @@ -62,7 +62,7 @@ val print_file : string -> (Format.formatter -> 'a) -> 'a (* ************************************************************************* *) type timer = float ref -type 'a result = Result of 'a | Error of exn +type 'a result = Result of 'a | Error of Printexc.raw_backtrace * exn val catch : ('a -> 'b) -> 'a -> 'b result val return : 'a result -> 'a val time : ?rmax:timer -> ?radd:timer -> ('a -> 'b) -> 'a -> 'b