Custom Query (361 matches)

[reported by Hendrik Tews on PG-devel list]

when you kill the currently active scripting buffer, then the hooks in proof-deactivate-scripting-hook are not run when the buffer was fully asserted. I believe this is a bug.

What happens is that

- kill-buffer-hook calls proof-script-kill-buffer-fn,
- which calls proof-deactivate-scripting-auto
- which calls (proof-deactivate-scripting 'process)
- which calls (proof-protected-process-or-retract 'process)
- which calls proof-process-buffer
- which calls (proof-assert-until-point-interactive)
- which calls proof-assert-until-point
- which throws 
     (error
	 "At end of the locked region, nothing to do to!"))
- this error unwinds until the ignore-errors in
 proof-deactivate-scripting-auto, thereby skipping the call to
 the hooks in proof-deactivate-scripting

The issue is that after changing the active scripting buffer, the first assert operation is lost, because the prover is not running. To reproduce go to coq/ex/test-cases/multiple-files-single-dir and do some scripting in, say, a.v. Then change to a different file (eg b.v) and do some scripting there. To clearly see the effect, make sure the second file (b.v) does not start with a comment.

There is a patch in ​http://lists.inf.ed.ac.uk/pipermail/proofgeneral-devel/2011/000114.html but it needs reviewing.

this was created without email verification.