no deactivation-hooks when killing fully asserted active buffer

[tews]

[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

[David Aspinall]

Fixed in CVS, proof-script.el 11.5