Custom Query (361 matches)

proof-retract-buffer fails to retract to the start of the theory, if there is any non-command material before the header, e.g. a comment.

Example:

(*blah*)
theory A imports Main begin

assert -- retract-buffer -- sync lost

BTW, it should be safe to issue the magic sequence init_toplevel; kill_thy A unconditionally, even if that theory has never really been started.

GMU Emacs 23.1.1, Mac OS.

Asserting a whole buffer via proof-process-buffer is very slow. One can watch the frontier of the locked region move in slow-motion. This is a MacPro? with 2.8 GHz and 8/16 cores (of course Emacs can use only 1 core anyway).

This is Mac OS X with the no-nonsense version of GNU Emacs 23.

Here proof-process-buffer does not give the usual incremental feedback, but finishes in a single shot (after quite some time of crunching as usual in PG).

It seems to work fine with the usual GNU Emacsen on Linux.