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/coqide.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/coqide.mli')
-rw-r--r-- | ide/coqide.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/coqide.mli b/ide/coqide.mli index cac6878cd..dd3995eb9 100644 --- a/ide/coqide.mli +++ b/ide/coqide.mli @@ -10,7 +10,7 @@ command line, initialize the load path, load the input state, load the files given on the command line, load the ressource file, produce the output state if any, and finally will launch the interface. *) -val sup_args : string ref +val sup_args : string list ref val do_load : string -> unit val process_argv : string list -> string list val crash_save : int -> unit |