Custom Query (361 matches)

Hello, here is how to reproduce the bug:

open a coq file (say toto.v). proof script one line. hit C-c C-x <enter> yes <enter>

and you get this:

Debugger entered--Lisp error: (error "Buffer toto.v has no process")

process-send-eof() scomint-send-eof() (if proof-shell-quit-cmd (scomint-send-string proc (concat proof-shell-quit-cmd "\n")) (scomint-send-eof)) (catch (quote exited) (set-process-sentinel proc (lambda ... ...)) (proof-deactivate-scripting-auto) (proof-shell-wait (proof-ass quit-timeout)) (if proof-shell-quit-cmd (scomint-send-string proc ...) (scomint-send-eof)) (let (... ...) (while ... ... ...)) (when (memq ... ...) (message "%s, cleaning up and exiting...killing process" bufname) (kill-process proc))) (progn (catch (quote exited) (set-process-sentinel proc ...) (proof-deactivate-scripting-auto) (proof-shell-wait ...) (if proof-shell-quit-cmd ... ...) (let ... ...) (when ... ... ...)) (set-process-sentinel proc nil)) (if (and alive proc) (progn (catch ... ... ... ... ... ... ...) (set-process-sentinel proc nil))) (when (and alive proc) (catch (quote exited) (set-process-sentinel proc ...) (proof-deactivate-scripting-auto) (proof-shell-wait ...) (if proof-shell-quit-cmd ... ...) (let ... ...) (when ... ... ...)) (set-process-sentinel proc nil)) (let* ((alive ...) (proc ...) (bufname ...)) (message "%s, cleaning up and exiting..." bufname) (redisplay t) (when (and alive proc) (catch ... ... ... ... ... ... ...) (set-process-sentinel proc nil)) (proof-script-remove-all-spans-and-deactivate) (proof-shell-clear-state) (run-hooks (quote proof-shell-kill-function-hooks)) (if (and proof-multiple-frames-enable proof-shell-fiddle-frames) (proof-delete-other-frames)) (let (...) (dolist ... ...)) (message "%s exited." bufname)) proof-shell-kill-function() kill-buffer(#<killed buffer>) (let ((kill-buffer-query-functions nil)) (kill-buffer proof-shell-buffer)) (progn (let (...) (kill-buffer proof-shell-buffer)) (setq proof-shell-buffer nil)) (if (or dont-ask (yes-or-no-p ...)) (progn (let ... ...) (setq proof-shell-buffer nil))) (when (or dont-ask (yes-or-no-p ...)) (let (...) (kill-buffer proof-shell-buffer)) (setq proof-shell-buffer nil)) (if (buffer-live-p proof-shell-buffer) (when (or dont-ask ...) (let ... ...) (setq proof-shell-buffer nil)) (error "No proof shell buffer to kill!")) proof-shell-exit() call-interactively(proof-shell-exit nil nil)

Currently, when there is a running prover process and user, hitting C-x C-c exits emacs without the usual user confirmation about process still running.

Hi,

the changeset 7913:9ebd4b14cadc committed on Oct 11 20:07:17 2010 +0200 breaks the cache. To reproduce, open the attached coq file and

1. do proof-process-buffer, which yields an error because there are two declarations peirce
2. change the first peirce into peirce_1 and do proof-process-buffer again. The error persists, because Proof General sent peirce instead of peirce_1 to the prover. Further the locked region ends in the middle of an identifier.

Bye,

Hendrik Tews