aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic/proof-menu.el
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2009-09-06 18:14:42 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2009-09-06 18:14:42 +0000
commit2a4f5dd47e2a8ceff78bcf695e59295ece79d3cb (patch)
treef73c7e840131d12a4d2c17eef06ae2f334ffdeb9 /generic/proof-menu.el
parentbe93117a3a7ea6af6f28b6631c3bcf04ec839f0a (diff)
Compile with cl. Fix typo.
Diffstat (limited to 'generic/proof-menu.el')
-rw-r--r--generic/proof-menu.el82
1 files changed, 42 insertions, 40 deletions
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index 53d692e8..23276241 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -7,6 +7,8 @@
;; $Id$
;;
+(require 'cl)
+
(require 'proof-utils) ; proof-deftoggle, proof-eval-when-ready-for-assistant
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -146,47 +148,47 @@ without adjusting window layout."
;;;###autoload
(defun proof-menu-define-specific ()
- (easy-menu-define
- proof-assistant-menu
- proof-mode-map
- (concat "The menu for " proof-assistant)
- (cons proof-assistant
- (append
- (proof-ass menu-entries)
- '("----")
- (or proof-menu-favourites
- (proof-menu-define-favourites-menu))
- (or proof-menu-settings
- (proof-menu-define-settings-menu))
- '("----")
- (list
- (vector
- (concat "Start " proof-assistant)
+ `(easy-menu-define
+ proof-assistant-menu
+ proof-mode-map
+ ,(concat "The menu for " proof-assistant)
+ ,(cons proof-assistant
+ (append
+ (proof-ass menu-entries)
+ '("----")
+ (or proof-menu-favourites
+ (proof-menu-define-favourites-menu))
+ (or proof-menu-settings
+ (proof-menu-define-settings-menu))
+ '("----")
+ (list
+ (vector
+ (concat "Start " proof-assistant)
'proof-shell-start
':active '(not (proof-shell-live-buffer)))
- (vector
- (concat "Exit " proof-assistant)
- 'proof-shell-exit
- ':active '(proof-shell-live-buffer))
- ;; TODO: doc <PA>-set-command here
- (vector
- (concat "Set " proof-assistant " command")
- (proof-ass-sym set-command)
- ':active '(fboundp (proof-ass-sym set-command))))
- '("----")
- (list
- (cons "Help"
- (append
- (list
- (vector
- (concat proof-assistant " information")
- 'proof-help
- :visible proof-info-command)
- (vector
- (concat proof-assistant " web page")
- '(browse-url proof-assistant-home-page)
- :visible proof-assistant-home-page))
- (proof-ass help-menu-entries))))))))
+ (vector
+ (concat "Exit " proof-assistant)
+ 'proof-shell-exit
+ ':active '(proof-shell-live-buffer))
+ ;; TODO: doc <PA>-set-command here
+ (vector
+ (concat "Set " proof-assistant " command")
+ (proof-ass-sym set-command)
+ ':active '(fboundp (proof-ass-sym set-command))))
+ '("----")
+ (list
+ (cons "Help"
+ (append
+ (list
+ (vector
+ (concat proof-assistant " information")
+ 'proof-help
+ :visible proof-info-command)
+ (vector
+ (concat proof-assistant " web page")
+ '(browse-url proof-assistant-home-page)
+ :visible proof-assistant-home-page))
+ (proof-ass help-menu-entries))))))))
(defun proof-assistant-menu-update ()
"Update proof assistant menu in scripting buffers."
@@ -832,7 +834,7 @@ KEY is the optional key binding."
;; pg-custom-undeclare-variable.
(if (assoc name proof-assistant-settings)
(progn
- (proof-debug "defpacustom: Proof assistanting setting %s re-defined!"
+ (proof-debug "defpacustom: Proof assistant setting %s re-defined!"
name)
(undefpgcustom name)))
(eval