diff options
| author | David Aspinall | 2000-05-30 11:24:18 +0000 |
|---|---|---|
| committer | David Aspinall | 2000-05-30 11:24:18 +0000 |
| commit | 223cc9e042618a228a88bda5e65a618e1a74ee04 (patch) | |
| tree | 81b5acafcf533d35ad8d61405fd1f766b949db1f /generic | |
| parent | 340963b38da050e85825f349f2e5eaf21a874612 (diff) | |
Added doc of new prefix arg feature for proof-minibuffer-cmd
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-script.el | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index f7eee781..7938e948 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1989,6 +1989,10 @@ 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 a prefix arg is given and there is a selected region, that is +pasted into the command. This is handy for copying terms, etc from +the script. + 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 |