Custom Query (361 matches)

GNU Emacs 23.1.1, Mac OS.

The point movement after asserting commands is still a bit odd. With proof-assert-next-command there is a higher change that it moves after the span than with proof-goto-point, where it seems to move to the span start unconditionally. But there are situations where both fail.

Also note that proof-goto-point does not work if the point is at the first position of the command keyword.

this was created without email verification.

I encountered a remaining issue with unicode support. Token \<one> is displayed as 1. When I copy this into another emacs buffer the information that this was \<one> is lost. The behaviour is OK for \<zero> which does not display as 0.

Suggested fix: \<one> should behave as \<zero> does.