Hi,
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
Bye,
Hendrik
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
