is there viewvc and cvshistory running on the Proof General cvs?
There's a handy view via Mercurial here courtesy of Markarius Wenzel
(hopefully he won't mind me advertising)
I've committed a patch to proof-protected-process-or-retract
now which fixes this problem and I think your test case works.
I don't see this. Here, coqtop still survives when I kill a
completely asserted active scripting buffer. The reason seems to
be that the unless now causes proof-protected-process-or-retract
to return nil and then the progn in
proof-deactivate-scripting-auto, which contains the deactivation
hooks, is skipped.
OK, let me take a look, I probably missed that the return value was
being used. I saw the killing but maybe it was happening at the wrong
moment which prompted my question below...
But there may be some further issues (try the coq autotest
OK, I do "make test.coq" and then I see some flickering and
finally emacs hangs. What is the proposed way to use the
Just as you did, Emacs shouldn't hang! But that might be a bug in the
test as I tried to put in a multiple file test. You can set
debug-on-signal to interrupt and get a backtrace.
coqtop is killed via proof-shell-exit inside
proof-deactivate-scripting-hook, that's inside the deactivation
action, isn't it?
but I'm seeing it being started
after switching buffers and beginning scripting somewhere
else, e.g. on the first non-comment element of the file.
Yes, that's the desired behavior: You can freely switch buffers,
but as soon as you start scripting in a buffer different from the
active scripting buffer, then the coptop process is killed.
OK, "as soon as you start scripting" includes comments, i.e. on making
the buffer active for scripting? That's what I expected (and maybe
what you intended!).
ProofGeneral-devel mailing list
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.