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

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++;