Hi Hendrik 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] - D. On 21 Jan 2011, at 07:42, Hendrik Tews wrote: > 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 > _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
