Functions find-and-forget and count-undos now return lists of commands

6 files changed, 23 insertions, 25 deletions

diff --git a/coq/coq.el b/coq/coq.el
index 2543eedd..8921ca82 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -306,7 +306,7 @@ used see coq-set-state-number. Initially 1 because Coq initial state has number
 (defun coq-set-state-infos ()
   "Set the last locked span's state number to the number found last time.
 This number is in the *last but one* prompt (variable `coq-last-but-one-statenum').
-If locked span already has a state number, thne do nothing. Also updates
+If locked span already has a state number, then do nothing. Also updates
 `coq-last-but-one-statenum' to the last state number for next time."
   (if (and proof-shell-last-prompt proof-script-buffer)
       ;; infos = promt infos of the very last prompt
@@ -387,10 +387,11 @@ If locked span already has a state number, thne do nothing. Also updates
              (equal coq-last-but-one-proofstack proofstack)
              (= coq-last-but-one-proofnum proofdepth)
              (= coq-last-but-one-statenum span-staten))
-      (format "Backtrack %s %s %s . "
-              (int-to-string span-staten)
-              (int-to-string proofdepth)
-              naborts))))
+      (list
+       (format "Backtrack %s %s %s . "
+               (int-to-string span-staten)
+               (int-to-string proofdepth)
+               naborts)))))
 
 (defvar coq-current-goal 1
   "Last goal that Emacs looked at.")
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 23dae667..de9f73e4 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -599,7 +599,7 @@ save commands, so don't use that if your prover has save commands."
   :group 'proof-script)
 
 (defcustom proof-count-undos-fn 'proof-generic-count-undos
-  "Function to calculate a command to issue undos to reach a target span.
+  "Function to calculate a list of command to undo to reach a target span.
 The function takes a span as an argument, and should return a string
 which is the command to undo to the target span.  The target is
 guaranteed to be within the current (open) proof.
@@ -611,7 +611,7 @@ settings `proof-non-undoables-regexp' and
   :group 'proof-script)
 
 (defcustom proof-find-and-forget-fn 'proof-generic-find-and-forget
-  "Function that returns a command to forget back to before its argument span.
+  "Function to return list of commands to forget to before its argument span.
 This setting is used to for retraction (undoing) in proof scripts.
 
 It should undo the effect of all settings between its target span
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 9438abc3..6435c373 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -2261,8 +2261,7 @@ up to the end of the locked region."
 	      (setq actions (proof-setup-retract-action
 			     start end
 			     (if (null span) nil ; was: proof-no-command
-			       ;; TODO: make proof-count-undos-fn return a list
-			       (list (funcall proof-count-undos-fn span)))
+			       (funcall proof-count-undos-fn span))
 			     delete-region)
 		    end start))
 	  ;; Otherwise, start the retraction by killing off the
@@ -2291,8 +2290,7 @@ up to the end of the locked region."
 	      ;; the target span.
 	      (nconc actions (proof-setup-retract-action
 			      start end
-			      ;; TODO: make `proof-find-and-forget-fn' return a list
-			      (list (funcall proof-find-and-forget-fn target))
+			      (funcall proof-find-and-forget-fn target)
 			      delete-region))))
 
     (proof-start-queue (min start end) (proof-locked-end) actions)))
@@ -2540,7 +2538,7 @@ assistant."
   (not (proof-string-match-safe proof-non-undoables-regexp cmd)))
 
 (defun proof-generic-count-undos (span)
-  "Count number of undos in SPAN, return command needed to undo that far.
+  "Count number of undos in SPAN, return commands needed to undo that far.
 Command is set using `proof-undo-n-times-cmd'.
 
 A default value for `proof-count-undos-fn'.
@@ -2564,9 +2562,9 @@ For this function to work properly, you must configure
     (if (= ct 0)
 	nil ; was proof-no-command
       (cond ((stringp proof-undo-n-times-cmd)
-	     (format proof-undo-n-times-cmd ct))
+	     (list (format proof-undo-n-times-cmd ct)))
 	    ((functionp proof-undo-n-times-cmd)
-	     (funcall proof-undo-n-times-cmd ct))))))
+	     (list (funcall proof-undo-n-times-cmd ct)))))))
 
 (defun proof-generic-find-and-forget (span)
   "Calculate a forget/undo command to forget back to SPAN.
@@ -2607,9 +2605,7 @@ with something different."
 	  (setq span nil)))
 	(if ans (setq answers (cons ans answers)))
 	(if span (setq span (next-span span 'type))))
-      (if (null answers)
-	  nil ; was proof-no-command
-	(apply 'concat answers))))))
+      answers))))
 
 ;;
 ;; End of new generic functions
diff --git a/isar/isar.el b/isar/isar.el
index 6c58e1eb..f75ff2a9 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -434,7 +434,7 @@ This is called when Proof General spots output matching
 		      (setq i (+ 1 i))))
 		   (t nil))))
       (setq span (next-span span 'type)))
-    (isar-undos isar-use-linear-undo ct)))
+    (list (isar-undos isar-use-linear-undo ct))))
 
 ;; undo theory commands
 (defun isar-find-and-forget (span)
@@ -474,8 +474,7 @@ This is called when Proof General spots output matching
 	(setq ans isar-undo)))
       (if ans (setq answers (cons ans answers)))
       (if span (setq span (next-span span 'type))))
-    (if (null answers) nil ; was proof-no-command
-       (apply 'concat answers))))
+    answers))
 
 (defun isar-goal-command-p (span)
   "Decide whether argument SPAN is a goal or not."
diff --git a/lego/lego.el b/lego/lego.el
index 92ef462a..2234bb12 100644
--- a/lego/lego.el
+++ b/lego/lego.el
@@ -187,8 +187,7 @@ Given is the first SPAN which needs to be undone."
 	       (if (= (aref str i) proof-terminal-char) (setq ct (+ 1 ct)))
 	       (setq i (+ 1 i)))))
       (setq span (next-span span 'type)))
-    ;; FIXME: make this stuff generic.  This should be undo-n-times-cmd
-    (concat "Undo " (int-to-string ct) ";")))
+    (list (concat "Undo " (int-to-string ct) ";"))))
 
 (defun lego-goal-command-p (span)
   "Decide whether argument is a goal or not"
@@ -231,7 +230,7 @@ Given is the first SPAN which needs to be undone."
       ;; Carry on searching forward for something to forget
       ;; (The first thing to be forget will forget everything following)
       (setq span (next-span span 'type)))
-  ans)); was (or ans proof-no-command)
+    (when ans (list ans)))); was (or ans proof-no-command)
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;   Other stuff which is required to customise script management   ;;
diff --git a/plastic/plastic.el b/plastic/plastic.el
index 546c9acb..047e20fb 100644
--- a/plastic/plastic.el
+++ b/plastic/plastic.el
@@ -228,7 +228,8 @@ Given is the first SPAN which needs to be undone."
 	       (if (= (aref string i) proof-terminal-char) (setq ct (+ 1 ct)))
 	       (setq i (+ 1 i)))))
       (setq span (next-span span 'type)))
-    (concat plastic-lit-string " &S Undo x" (int-to-string ct) proof-terminal-string)))
+    (list (concat plastic-lit-string 
+		  " &S Undo x" (int-to-string ct) proof-terminal-string))))
 
 (defun plastic-goal-command-p (span)
   "Decide whether argument is a goal or not"			;; NEED CHG.
@@ -266,7 +267,9 @@ Given is the first SPAN which needs to be undone."
       (setq span (next-span span 'type))
 
     )
-    (concat plastic-lit-string " &S Undo x" (int-to-string spans) proof-terminal-string) ))
+    (list (concat plastic-lit-string 
+		  " &S Undo x" (int-to-string spans) 
+		  proof-terminal-string))))
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;   Other stuff which is required to customise script management   ;;