| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
|
| |
Julien Narboux confirmed that it was dead code (GeoProof is not to be
confused with GeoCoq).
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Threads were only there to handle blocking dialogs with the different
coqtops. But programming with threads have drawbacks : complex mutex
infrastructure, possible deadlocks, etc. In particular gtk functions
are not meant to be called from a thread which isn't the gtk main loop,
(unless some gtk mutex have been taken). This seem to pose problem
specifically in win32 (and macosx ?), hence the use of the
GtkThread.(a)sync hack for scheduling code for execution in the gtk
main loop.
Instead, we now use the Glib.Io module to install a callback that will
be runned when some answer of coqtop is available on the channel.
This implies using now a continuation-passing style: for instance,
instead of two sequential requests to coqtop, we'll now have the
2nd request inside the callback handling the answer to the 1st request.
Remarks:
- Also use asynchronous i/o for external commands (editor, coqc, make...).
Launching an external editor or browser won't freeze coqide anymore.
- Reworked handling of coqtop process, especially when closing them.
A responsive coqtop should now hara-kiri immediatly when its input
channel is closed. Otherwise we try later a soft kill, then some
hard kills if necessary. If nothing work we warns the user.
When quitting coqide, all this might induce a small delay (2s at worse).
- Be careful now to avoid "long" computations (or blocking i/o) in
a coqide function. Experimentally, it seems that loading/saving a .v
file is quick enough. If necessary, we could use asynchronous i/o
also for writing the .v, but for loading I've no clue.
- In the Coqide module, we ensure that the current continuation k
will indeed be run at the end thanks to an abstract return type
(void = opaque copy of unit).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16049 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
We now try harder to handle ourselves gtk messages (e.g. Gtk-WARNING ...).
This way, we could reroute them nicely in w32, and pop-up the critical ones.
Moreover, the code rerouting debug messages to a log file in w32 was using
!Ideutils.debug before its initialization. Now, when a log file is used, its
name is displayed in the about messages.
Btw, some code cleaning in coqide_main
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16037 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
| |
Ctrl-C now triggers a clean (interactive) quit.
The other catchable signals still trigger an emergency (non-interactive) quit.
Btw, stop trying to relaunch the gtk loop in case of failure
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16036 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15325 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
| |
to specify where to look the project file
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14441 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
| |
It now checks for 5 sec every 0.1 sec if is there is still running coqtop
then it asks the user if he wants to leave zombies or cancel quit.
(Cancel quit was continue to wait).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13973 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
When using "Goto start" while many phrases are evaluated,
it's frequent with earlier code that the restart occurs
between two phrases, and hence the second is sent to the new
coqtop, triggering things like "Anomaly: NoCurrentProof".
To avoid that, Coq.coqtop is now immutable (no silent switch
of channels). In Coqide, toplvl and mycoqtop are now references,
that are updated when using reset_coqtop.
We organize things in order to have only one access to mycoqtop
during code that does many sequential calls to coqtop. This way,
when coqtop changes, the code speaks to the old one, and gets
some exception when writing/reading on a close channel.
By the way, some documentation, cleanup, etc etc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13942 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
* Run "coqide -coqtop someothercoqtop" if you want to use a toplevel
which isn't the one coming alongside coqide. To be documented,
to be improved (maybe an field in coqide's preferences ?).
coqide -h should display this kind of ide-specific option.
* Since we now use create_process instead of open_process, we don't
use /bin/sh, hence running Filename.quote on args was actually
wrong.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13932 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
- 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
|
| |
|
|
|
|
|
| |
if `pkg-config --exists ige-mac-integration`, coqide.opt will be
able to open files by double-clik in finder on Darwin.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13779 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
|
|
|
|
|
|
|
| |
- Many of them were broken, some of them after Pierre B's rework
of mli for ocamldoc, but not only (many bad annotation, many files
with no svn property about Id, etc)
- Useless for those of us that work with git-svn (and a fortiori
in a forthcoming git-only setting)
- Even in svn, they seem to be of little interest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6621 85f007b7-540e-0410-9357-904b9bb8a0f7
|
| |
|
|
| |
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
|
|
|
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3995 85f007b7-540e-0410-9357-904b9bb8a0f7
|
Théo Zimmermann
Maxime Dénès
Pierre-Marie Pédrot
letouzey
herbelin
pboutill
glondu
monate