Yes, it looks like a bad path, probably not noticeable before since we've used
the hook for functions that only are useful when the shell is live.
Do you want to repair by adding a test for fully processed buffer?
[Or I can do, but not until much later today]
On 21 Jan 2011, at 07:42, Hendrik Tews wrote:
> 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
> "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
> ProofGeneral-devel mailing list
ProofGeneral-devel mailing list
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.