diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-03-23 17:18:55 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-03-23 17:18:55 +0000 |
| commit | 461798eeecfd2a59159fb9666874d8ea14209624 (patch) | |
| tree | 5e8bc059ef5743622fa1fbbdf45145e2a2d23294 /ide/coq.mli | |
| parent | 150f9c3cfd32e1e0ed71d11644614a6cab1621a7 (diff) | |
Ide: experimentally allow coqide to interrupt or kill coqtop
- We now use create_process instead of open_process, and stores
the answered pid.
- The "Stop" button now sends a Sigint signal to this coqtop pid.
- The "Goto Start" button now works even if a computation is ongoing,
a new process is spawned and the previous one is killed -9, and
then a waitpid is done to avoid having zombies around.
Note that currently a vm_compute won't be stopped by a "Stop",
but only by a "Goto Start". This can be quite confusing. How to
properly document that "Goto Start" has the side effect of being
a kill ? Maybe we could check someday if the Ctrl-C has been
successful, and kill -9 if not ? Or maybe make coqide aware
of a flag "we_are_vm_computing" and then kill -9 instead of Ctrl-C
in this case ?
TODO:
- for the moment a forced "Goto Start" displays an unfriendly anomaly
- check if all this works under Windows (probably but not sure).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13926 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide/coq.mli')
| -rw-r--r-- | ide/coq.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/ide/coq.mli b/ide/coq.mli index 6bc593477..c909a559f 100644 --- a/ide/coq.mli +++ b/ide/coq.mli @@ -15,16 +15,16 @@ open Ide_blob val short_version : unit -> string val version : unit -> string val filter_coq_opts : string list -> bool * string list -val check_connection : string -> unit +val check_connection : string list -> unit type coqtop -val dummy_coqtop : coqtop - -val spawn_coqtop : string -> coqtop +val spawn_coqtop : string list -> coqtop val kill_coqtop : coqtop -> unit +val break_coqtop : coqtop -> unit + val coqtop_zombies : unit -> int val reset_coqtop : coqtop -> unit |