diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2009-09-05 09:54:56 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2009-09-05 09:54:56 +0000 |
| commit | b30f353c2ea9f514d7ab6bf821a7919adf62143a (patch) | |
| tree | 9fe25f3ed35c8377d749d8e7336c9e44fd7481e6 /generic/pg-goals.el | |
| parent | 559426016c112b6147fe82582c6479521b0fab6a (diff) | |
Clean whitespace
Diffstat (limited to 'generic/pg-goals.el')
| -rw-r--r-- | generic/pg-goals.el | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/generic/pg-goals.el b/generic/pg-goals.el index e3e53c5a..a0b125a4 100644 --- a/generic/pg-goals.el +++ b/generic/pg-goals.el @@ -58,7 +58,7 @@ May enable proof-by-pointing or similar features. (define-key proof-goals-mode-map [q] 'bury-buffer) ;; TODO: use standard Emacs button behaviour here (cf Info mode) (define-key proof-goals-mode-map [mouse-1] 'pg-goals-button-action) -(define-key proof-goals-mode-map [C-mouse-3] +(define-key proof-goals-mode-map [C-mouse-3] 'proof-undo-and-delete-last-successful-command) @@ -81,14 +81,14 @@ Converts term substructure markup into mouse-highlighted extents." (save-excursion ;; Response buffer may be out of date. It may contain (error) ;; messages relating to earlier proof states - + ;; NB: this isn't always the case. In Isabelle ;; we get <WARNING MESSAGE> <CURRENT GOALS> output, ;; or <WARNING MESSAGE> <ORDINARY MESSAGE>. Both times ;; <WARNING MESSAGE> would be relevant. ;; We should only clear the output that was displayed from ;; the *previous* prompt. - + ;; Erase the response buffer if need be, maybe removing the ;; window. Indicate it should be erased before the next output. (pg-response-maybe-erase t t) @@ -105,7 +105,7 @@ Converts term substructure markup into mouse-highlighted extents." (insert string) (setq buffer-read-only t) (set-buffer-modified-p nil) - + ;; Keep point at the start of the buffer. (proof-display-and-keep-buffer proof-goals-buffer (point-min))))) @@ -125,14 +125,14 @@ Converts term substructure markup into mouse-highlighted extents." (cond (sendback (with-current-buffer buf - (let* ((cmdstart (previous-single-property-change pos 'sendback + (let* ((cmdstart (previous-single-property-change pos 'sendback nil (point-min))) - (cmdend (next-single-property-change pos 'sendback + (cmdend (next-single-property-change pos 'sendback nil (point-max))) (cmd (buffer-substring-no-properties cmdstart cmdend))) (proof-insert-sendback-command cmd))))))) - + |