diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2010-08-15 23:11:38 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2010-08-15 23:11:38 +0000 |
| commit | 0b1ce1bd821974f68f683ec858a7a2fdd0fd49ea (patch) | |
| tree | 4796a2eab6836f7dcdca4c5f9c8fc00f31152e77 /generic/pg-user.el | |
| parent | f413ef7a0ddad7ce6969db1914f3c75b01051db4 (diff) | |
proof-issue-new-command: remove spurious goto-char (ref Trac #330)
Diffstat (limited to 'generic/pg-user.el')
| -rw-r--r-- | generic/pg-user.el | 8 |
1 files changed, 1 insertions, 7 deletions
diff --git a/generic/pg-user.el b/generic/pg-user.el index f8b2c265..ac2a3210 100644 --- a/generic/pg-user.el +++ b/generic/pg-user.el @@ -438,14 +438,8 @@ Start up the proof assistant if necessary." (if (proof-in-locked-region-p) (proof-goto-end-of-locked t))) (proof-script-new-command-advance) - ;; FIXME: fixup behaviour of undo here. Really want to temporarily - ;; disable undo for insertion. but (buffer-disable-undo) trashes - ;; whole undo list! (insert cmd) - ;; FIXME: could do proof-indent-line here, but let's wait until - ;; indentation is fixed. - (goto-char - (proof-assert-until-point-interactive)) + (proof-assert-until-point-interactive) (proof-script-new-command-advance))) ;; |