From 6fc78f750494d5ec0d677e42fb1d3651427b13a9 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Wed, 7 Oct 1998 16:19:01 +0000 Subject: Removed coq-settings defgroup, changed to coq. Defcustom'd coq-prog-name. Removed proof-assistant setting (now automatic) Added FIXME question about proof-shell-init-cmd. --- coq/coq.el | 23 +++++++++-------------- 1 file changed, 9 insertions(+), 14 deletions(-) diff --git a/coq/coq.el b/coq/coq.el index 60dfcb14..6587a9da 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -15,17 +15,10 @@ (setq tag-always-exact t) ; Tags is unusable with Coq library otherwise: -(defgroup coq-settings nil - "Customization of Coq specific settings for Proof General." - :group 'proof-general) - -(defvar coq-assistant "Coq" - "Name of proof assistant") - (defcustom coq-tags "/usr/local/lib/coq/theories/TAGS" "the default TAGS table for the Coq library" :type 'string - :group 'coq-settings) + :group 'coq) (defconst coq-process-config nil "Command to configure pretty printing of the Coq process for emacs.") @@ -36,19 +29,21 @@ (defcustom coq-default-undo-limit 100 "Maximum number of Undo's possible when doing a proof." :type 'number - :group 'coq-settings) + :group 'coq) ;; ----- web documentation (defcustom coq-www-home-page "http://pauillac.inria.fr/coq/" "Coq home page URL." :type 'string - :group 'coq-settings) + :group 'coq) ;; ----- coq-shell configuration options -(defvar coq-prog-name "coqtop -emacs" - "*Name of program to run as Coq.") +(defcustom coq-prog-name "coqtop -emacs" + "*Name of program to run as Coq." + :type 'string + :group 'coq) (defvar coq-shell-prompt-pattern (concat "^" proof-id " < ") "*The prompt pattern for the inferior shell running coq.") @@ -105,6 +100,7 @@ ;; Code that's coq specific ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; FIXME da: can't this be done by proof-shell-init-cmd ? (defun coq-shell-init-hook () (insert (format "Set Undo %s." coq-default-undo-limit)) (insert (format "Cd \"%s\"." default-directory)) @@ -309,8 +305,7 @@ (setq proof-comment-start "(*") (setq proof-comment-end "*)") - (setq proof-assistant coq-assistant - proof-www-home-page coq-www-home-page) + (setq proof-www-home-page coq-www-home-page) (setq proof-prf-string "Show" proof-ctxt-string "Print All" -- cgit v1.2.3