From 0b1ce1bd821974f68f683ec858a7a2fdd0fd49ea Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Sun, 15 Aug 2010 23:11:38 +0000
Subject: proof-issue-new-command: remove spurious goto-char (ref Trac #330)

---
 generic/pg-user.el | 8 +-------
 1 file changed, 1 insertion(+), 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)))
 
 ;;
-- 
cgit v1.2.3