aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-04-01 13:17:13 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-04-01 13:17:13 +0000
commit86eda408ad28a80a33ae31743e9ae77ceb7967c2 (patch)
tree9be9db5d77b90b63469459016816d04896248efd /kernel
parent7d497e25f19022aa7f697cffb353f9f6776e822e (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.c14
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++;