aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/csymtable.ml
diff options
context:
space:
mode:
authorGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-01-28 21:05:51 +0000
committerGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2013-01-28 21:05:51 +0000
commit1ce2c89e8fd2f80b49fcac9e045667b7233391ef (patch)
tree2c74cfaebbe65f5c1a455040aaae3dd173ff4425 /kernel/csymtable.ml
parent5a39e6c08d428d774165e0ef3922ba8b75eee9e1 (diff)
Added backtrace primitives.
Using OCaml 3.11+ builtin facilities to record stack frames during exception raising, we can now recover at runtime the backtrace of an uncaught toplevel exception and display it to the user, without the infamous OCaml debugger. The backtrace is displayed when using the [-debug] flag. This requires a bit of discipline, as each time we reraise an exception we need to keep track of those frames we discarded between the previous raise and the current [try-with] branch. Currently, only [Anomaly] is handled, but this can be ported to any exception as long as we add the backtrace info into the exception, and we provide the corresponding handler to [Backtracke.register_backtrace_handler]. Hopefully this should not be to costly, as we only do little work when reraising, and only with the [-debug] flag set. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16166 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/csymtable.ml')
0 files changed, 0 insertions, 0 deletions