Last active
November 12, 2018 15:19
-
-
Save Chobbes/bb61319bf410698a8ddf3d8778130949 to your computer and use it in GitHub Desktop.
Make proof-general's next command put the cursor at the end of the next unprocessed command
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| (defun proof-assert-after-next-command () | |
| (interactive) | |
| (proof-assert-next-command-interactive) | |
| (let* ((segment (car (proof-segment-up-to-using-cache (point)))) | |
| (type (car segment)) | |
| (command-end (- (caddr segment) (if (eq type 'comment) 2 1)))) | |
| (goto-char command-end))) | |
| (eval-after-load "proof-script" | |
| '(progn | |
| (define-key proof-mode-map (kbd "C-<down>") 'proof-assert-after-next-command) | |
| (define-key proof-mode-map (kbd "C-<up>") 'proof-undo-last-successful-command))) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment