diff options
| -rw-r--r-- | coq/coq.el | 6 | ||||
| -rw-r--r-- | generic/proof-config.el | 9 | ||||
| -rw-r--r-- | isar/isar-syntax.el | 2 | ||||
| -rw-r--r-- | isar/isar.el | 3 | ||||
| -rw-r--r-- | lego/lego.el | 2 | ||||
| -rw-r--r-- | phox/phox-fun.el | 2 |
6 files changed, 10 insertions, 14 deletions
@@ -498,7 +498,7 @@ If locked span already has a state number, thne do nothing. Also updates (int-to-string span-staten) (int-to-string proofdepth) naborts))) - (if (string-equal ans "") proof-no-command ; not here because if + (if (string-equal ans "") nil ; [was proof-no-command]not here because if ;; we backtrack a state preserving command, we must do ;; *nothing*, not even a CR (in > v74, no prompt is returned ;; with "\n") @@ -592,8 +592,8 @@ If locked span already has a state number, thne do nothing. Also updates (if (> nundos 0) (concat "Undo " (int-to-string nundos) ". ")))) - (if (null ans) proof-no-command;; FIXME: this is an error really (assert nil); - (if (string-equal ans "") proof-no-command ; not here because if + (if (null ans) nil;; [was proof-no-command] FIXME: this is an error really (assert nil); + (if (string-equal ans "") nil ;; [was proof-no-command] ; not here because if ; we backtrack a state preserving command, we must do ; *nothing*, not even a CR (in v74, no prompt is returned ; with "\n") diff --git a/generic/proof-config.el b/generic/proof-config.el index c83a9dd3..2bd15a77 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -611,11 +611,6 @@ settings `proof-non-undoables-regexp' and :type 'function :group 'proof-script) -(defconst proof-no-command "COMMENT" - "String used as a nullary action (send no command to the proof assistant). -Only relevant for `proof-find-and-forget-fn'. -\(NB: this is a CONSTANT, don't change it).") - (defcustom proof-find-and-forget-fn 'proof-generic-find-and-forget "Function that returns a command to forget back to before its argument span. This setting is used to for retraction (undoing) in proof scripts. @@ -624,7 +619,7 @@ It should undo the effect of all settings between its target span up to (proof-locked-end). This may involve forgetting a number of definitions, declarations, or whatever. -The special string `proof-no-command' means there is nothing to do. +If return value is nil, it means there is nothing to do. This is an important function for script management. Study one of the existing instantiations for examples of how to write it, @@ -1070,7 +1065,7 @@ Normally error messages cause a beep. Set this to nil to prevent that." ;; (defcustom proof-shell-prompt-pattern nil - "Proof shell's value for comint-prompt-pattern, which see. + "Proof shell's value for `comint-prompt-pattern', which see. NB!! This pattern is just for interaction in comint (shell buffer). You don't really need to set it. The important one to set is `proof-shell-annotated-prompt-regexp', which see." diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el index 3cf66850..1af9e545 100644 --- a/isar/isar-syntax.el +++ b/isar/isar-syntax.el @@ -461,7 +461,7 @@ matches contents of quotes for quoted identifiers.") (defun isar-undos (i) (if (> i 0) (concat "undos_proof " (int-to-string i) ";") - proof-no-command)) + nil)) ; was proof-no-command (defun isar-cannot-undo (cmd) (concat "cannot_undo \"" cmd "\";")) diff --git a/isar/isar.el b/isar/isar.el index 5014fc9b..bfe635d0 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -456,7 +456,8 @@ 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) proof-no-command (apply 'concat answers)))) + (if (null answers) nil ; was proof-no-command + (apply 'concat 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 d6211edb..896309f0 100644 --- a/lego/lego.el +++ b/lego/lego.el @@ -237,7 +237,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))) - (or ans proof-no-command))) + ans)); was (or ans proof-no-command) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Other stuff which is required to customise script management ;; diff --git a/phox/phox-fun.el b/phox/phox-fun.el index 6471f3d4..82531470 100644 --- a/phox/phox-fun.el +++ b/phox/phox-fun.el @@ -243,7 +243,7 @@ or for optional argument TABLE." (setq lsp (span-start span)) (setq span (next-span span 'type))) - (or ans proof-no-command))) + ans)) ; was (or ans proof-no-command) ;; ;; Doing commands |