diff options
Diffstat (limited to 'generic/proof-script.el')
| -rw-r--r-- | generic/proof-script.el | 21 |
1 files changed, 12 insertions, 9 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index 1a677434..cbc0e80a 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1980,17 +1980,20 @@ This is a subroutine used in proof-shell-handle-{error,interrupt}." "Prompt for a command in the minibuffer and send it to proof assistant. The command isn't added to the locked region. -If `proof-state-preserving-p' is configured, it is used as a check -that the command will be safe to execute, in other words, that -it won't ruin synchronization. If when applied to the command it -returns false, then an error message is given. - -This command risks spoiling synchronization if the test -`proof-state-preserving-p' is not configured, or if it is -only an approximate test." +If `proof-strict-state-preserving' is set, and `proof-state-preserving-p' +is configured, then the latter is used as a check that the command +will be safe to execute, in other words, that it won't ruin +synchronization. If when applied to the command it returns false, +then an error message is given. + +WARNING: this command risks spoiling synchronization if the test +`proof-state-preserving-p' is not configured, if it is +only an approximate test, or if `proof-strict-state-preserving' +is off (nil)." (interactive (list (read-string "Command: " nil 'proof-minibuffer-history))) - (if (and proof-state-preserving-p + (if (and proof-strict-state-preserving + proof-state-preserving-p (not (funcall proof-state-preserving-p cmd))) (error "Command is not state preserving, I won't execute it!")) (proof-shell-invisible-command cmd)) |