From 5763eb8f7874589a77fd079b7d196fd515930c4e Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Thu, 17 Jan 2008 13:03:24 +0000 Subject: Use featurep test for XEmacs. Set proof-shell-indentifier-under-mouse-cmd. --- coq/coq.el | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/coq/coq.el b/coq/coq.el index 05ffbe6e..0b59d16a 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -824,20 +824,20 @@ This is specific to `coq-mode'." ;; FIXME da: Does Coq have a help or about command? ;; proof-info-command "Help" -;; 3.4: this is no longer used: setting to nil -;; enforces use of find-and-forget always. + ;; 3.4: this is no longer used: setting to nil + ;; enforces use of find-and-forget always. (setq proof-kill-goal-command nil) (setq proof-goal-command-p 'coq-goal-command-p proof-find-and-forget-fn 'coq-find-and-forget pg-topterm-goalhyplit-fn 'coq-goal-hyp - proof-state-preserving-p 'coq-state-preserving-p - ) + proof-state-preserving-p 'coq-state-preserving-p) ;; This one to deal with nested comments in xemacs - (if (string-match "XEmacs" emacs-version) - (setq proof-script-parse-function 'coq-parse-function) - ) + (if (featurep 'xemacs) + (setq proof-script-parse-function 'coq-parse-function)) + + (setq proof-shell-indentifier-under-mouse-cmd "Check %s.") (setq proof-save-command-regexp coq-save-command-regexp proof-really-save-command-p 'coq-save-command-p ;pierre:deals with Proof . @@ -1391,7 +1391,6 @@ be asked to the user." (interactive) (coq-insert-from-db coq-terms-db "Kind of term")) - (define-key coq-keymap [(control ?i)] 'coq-insert-intros) (define-key coq-keymap [(control ?m)] 'coq-insert-match) (define-key coq-keymap [(control ?()] 'coq-insert-section-or-module) -- cgit v1.2.3