diff options
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-config.el | 4 | ||||
| -rw-r--r-- | generic/proof-script.el | 16 |
2 files changed, 8 insertions, 12 deletions
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 |