diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-01 13:17:13 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-01 13:17:13 +0000 |
commit | 86eda408ad28a80a33ae31743e9ae77ceb7967c2 (patch) | |
tree | 9be9db5d77b90b63469459016816d04896248efd /kernel | |
parent | 7d497e25f19022aa7f697cffb353f9f6776e822e (diff) |
Checks for signals in VM, allowing it to be interrupted by Ctrl-C (experimental)
We simply reuse the ocaml flag caml_signals_are_pending and the function
caml_process_pending_signals, and place a test at some place of the interpreter
loop (at a similar location as in ocaml byterun/interp.c).
The symbols caml_* we use are not officially made public in *.h installed
alongside ocaml, but they seem pretty stable (there since at least
ocaml 3.10, independent of arch and of byte/asm), so we access them via
"extern". For once, thanks dirty C...
In addition to that, when catching a Ctrl-C, we reset the vm via
"coq_sp = coq_stack_high" as suggested by Benjamin G.
This patch should be quite portable, it might even work in win32.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13947 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/byterun/coq_interp.c | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index a45183f30..842ac5619 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -14,6 +14,7 @@ for fast computation of bounded (31bits) integers */ #include <stdio.h> +#include <signal.h> #include "coq_gc.h" #include "coq_instruct.h" #include "coq_fix_code.h" @@ -150,6 +151,12 @@ sp is a local copy of the global variable extern_sp. */ #endif #endif +/* For signal handling, we highjack some code from the caml runtime */ + +extern intnat caml_signals_are_pending; +extern intnat caml_pending_signals[]; +extern void caml_process_pending_signals(void); + /* The interpreter itself */ value coq_interprete @@ -407,8 +414,13 @@ value coq_interprete realloc_coq_stack(Coq_stack_threshold); sp = coq_sp; } + /* We also check for signals */ + if (caml_signals_are_pending) { + /* If there's a Ctrl-C, we reset the vm */ + if (caml_pending_signals[SIGINT]) { coq_sp = coq_stack_high; } + caml_process_pending_signals(); + } Next; - /* Fall through CHECK_SIGNALS */ Instruct(APPTERM) { int nargs = *pc++; |