diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-01-28 21:05:51 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-01-28 21:05:51 +0000 |
| commit | 1ce2c89e8fd2f80b49fcac9e045667b7233391ef (patch) | |
| tree | 2c74cfaebbe65f5c1a455040aaae3dd173ff4425 /checker/check.mllib | |
| parent | 5a39e6c08d428d774165e0ef3922ba8b75eee9e1 (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 'checker/check.mllib')
| -rw-r--r-- | checker/check.mllib | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/checker/check.mllib b/checker/check.mllib index 1bc23734a..2d56e163b 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -1,4 +1,5 @@ Coq_config +Backtrace Int Pp_control Flags |