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 <[email protected]> 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 [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
