diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2000-05-05 11:29:18 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2000-05-05 11:29:18 +0000 |
| commit | 4a693dadd0e28c03bc19637238894ff89ca05e6c (patch) | |
| tree | 09993a2610541d76e08a7d1d57894b0bebac2d51 /generic/proof-toolbar.el | |
| parent | e6770fe99299f8b5d1093ad0b44632d1d3705991 (diff) | |
Added menu entry for proof-goto-end-of-locked.
Diffstat (limited to 'generic/proof-toolbar.el')
| -rw-r--r-- | generic/proof-toolbar.el | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/generic/proof-toolbar.el b/generic/proof-toolbar.el index 984bfbd2..c4cb9ca0 100644 --- a/generic/proof-toolbar.el +++ b/generic/proof-toolbar.el @@ -53,6 +53,7 @@ (goto "Goto point" "Process or undo to the cursor position" t) (restart "Restart scripting" "Restart scripting (clear all locked regions)" t) (qed "Finish proof" "Close/save proved theorem" t) + (lockedend "Locked end" nil t) (find "Find theorems" "Find theorems" t) (command "Issue command" "Issue a non-scripting command" t) (interrupt "Interrupt prover" "Interrupt the proof assistant (warning: may break synchronization)" t) @@ -288,6 +289,16 @@ changed state." (defalias 'proof-toolbar-delete 'proof-undo-and-delete-last-successful-command) +;; +;; Lockedend button (not actually on toolbar) +;; + +(defun proof-toolbar-lockedend-enable-p () + t) + +(defalias 'proof-toolbar-lockedend 'proof-goto-end-of-locked) + + ;; |