Hi,

is there viewvc and cvshistory running on the Proof General cvs?
(Like, for example,
http://www.sos.cs.ru.nl/cgi-bin/~tews/olmar/viewvc-patch.cgi/elsa/
and http://www.sos.cs.ru.nl/cgi-bin/~tews/olmar/cvshistory.cgi)

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
   script) 

OK, I do "make test.coq" and then I see some flickering and
finally emacs hangs. What is the proposed way to use the
autotest? 

   I don't quite understand the places where this happens: it
   would seem cleanest if the process was started/exited with the
   activate/deactivate action, 

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.

Bye,

Hendrik
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel

Reply via email to