From 152e80c7a4a30fa3432ca9232faf33e32bfd80e5 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Mon, 14 Sep 2009 23:31:44 +0000
Subject: Fix compile issues

---
 generic/proof-script.el | 23 ++++++++++++++++++++---
 1 file changed, 20 insertions(+), 3 deletions(-)

(limited to 'generic')

diff --git a/generic/proof-script.el b/generic/proof-script.el
index 7472743b..9db446d0 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1370,11 +1370,12 @@ Argument SPAN has just been processed."
     (and proof-save-with-hole-regexp
 	 (proof-string-match proof-save-with-hole-regexp cmd)
 	 ;; Give a message of a name if one can be determined
-	 (proof-minibuffer-message "proved %s"
+	 (proof-minibuffer-message 
+	  (format "proved %s"
 		  (setq nam
 			(if (stringp proof-save-with-hole-result)
 			    (replace-match proof-save-with-hole-result nil nil cmd)
-			  (match-string proof-save-with-hole-result cmd)))))
+			  (match-string proof-save-with-hole-result cmd))))))
 
     ;; Search back for a goal command, deleting spans along the way:
     ;; they may be amalgamated into a single goal-save region, which
@@ -1982,6 +1983,22 @@ each queue item."
 
 
 
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
+;; Moving point in proof script buffer
+;;
+
+(defun proof-script-next-command-advance ()
+  "Move point to the beginning of the next command if it's nearby.
+Assumes that point is at the end of a command."
+  (interactive)
+  (skip-chars-forward " \t\n"))
+;  (if (and proof-one-command-per-line (eolp))
+;      (forward-line)))
+
+
+
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
@@ -2038,7 +2055,7 @@ comment, and insert or skip to the next semi)."
 	      (goto-char mrk)
 	      (insert proof-terminal-string))
 	  ;; assert a region
-	  (proof-assert-semis semis startpos)
+	  (proof-assert-semis semis)
 	  (proof-script-next-command-advance))))))
 
 (defun proof-assert-semis (semis) 
-- 
cgit v1.2.3