diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 1998-11-03 14:37:48 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 1998-11-03 14:37:48 +0000 |
| commit | 5a271121d0bdd20f535b3038a9831fdcfde67b0e (patch) | |
| tree | bc275c7c18edd173ae23f2f7c4fa45c642f84f79 /generic/proof-script.el | |
| parent | d36aa837d21c8323b1bbe4fcf4f34f9688122018 (diff) | |
Renamed a couple of menu functions in case of later making
proof-menu.el. Always call proof-toolbar-setup.
Diffstat (limited to 'generic/proof-script.el')
| -rw-r--r-- | generic/proof-script.el | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index 2b6de678..cefcbd39 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1257,12 +1257,12 @@ Start up the proof assistant if necessary." ;;; To be called from menu -(defun proof-info-mode () +(defun proof-menu-invoke-info () "Call info on Proof General." (interactive) (info "ProofGeneral")) -(defun proof-exit () +(defun proof-menu-exit () "Exit Proof-assistant." (interactive) (proof-restart-script)) @@ -1273,7 +1273,7 @@ Start up the proof assistant if necessary." (browse-url proof-assistant-home-page) t] ["Proof General home page" (browse-url proof-proof-general-home-page) t] - ["Proof General Info" proof-info-mode t] + ["Proof General Info" proof-menu-invoke-info t] ) "The Help Menu in Script Management.") @@ -1285,7 +1285,7 @@ Start up the proof assistant if necessary." :active (proof-shell-live-buffer)] ["Display proof state" proof-prf :active (proof-shell-live-buffer)] - ["Exit proof assistant" proof-exit + ["Exit proof assistant" proof-menu-exit :active (proof-shell-live-buffer)]) (if proof-tags-support (list @@ -1301,7 +1301,7 @@ Start up the proof assistant if necessary." :style toggle :selected proof-active-terminator-minor-mode] "----") - ;; UGLY COMPATIBILITY + ;; UGLY COMPATIBILITY FIXME: remove this soon (list (if (string-match "XEmacs 19.1[2-9]" emacs-version) "--:doubleLine" "----")) proof-shared-menu @@ -1476,9 +1476,10 @@ finish setup which depends on specific proof assistant configuration." (make-local-variable 'indent-line-function) (setq indent-line-function 'proof-indent-line) + ;; Toolbar - (if (featurep 'toolbar) - (proof-toolbar-setup)) + ;; (NB: autloads proof-toolbar, which extends proof-menu variable) + (proof-toolbar-setup) ;; Menu (easy-menu-define proof-mode-menu |