is there viewvc and cvshistory running on the Proof General cvs?
(Like, for example,
David Aspinall <david.aspin...@ed.ac.uk> writes:
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.
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
I don't quite understand the places where this happens: it
would seem cleanest if the process was started/exited with the
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.
ProofGeneral-devel mailing list