Move defpacustom here. Move message functions to proof-shell. Fix requires.

1 files changed, 98 insertions, 16 deletions

diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index 0218c823..7a1ac808 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -15,6 +15,11 @@
 ;;
 
 (require 'proof-site)			; basic vars
+(require 'proof-compat)		        ; compatibility
+(require 'proof-config)			; config vars
+(require 'bufhist)			; bufhist
+(require 'proof-syntax)			; syntax utils
+(require 'proof-autoloads)		; interface fns
 (require 'scomint)			; for proof-shell-live-buffer
 
 
@@ -49,11 +54,8 @@
 
 
 (require 'proof-compat)		        ;
-(require 'proof-config)			; config vars
 (require 'bufhist)			; bufhist
-(require 'proof-syntax)			; syntax utils
-(require 'proof-autoloads)		; interface fns
-
+;(require 'proof-syntax)			; syntax utils
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
@@ -210,7 +212,7 @@ If NEWVAL is present, set the variable, otherwise return its current value.")
 (defmacro defpgcustom (sym &rest args)
   "Define a new customization variable <PA>-SYM for the current proof assistant.
 The function proof-assistant-<SYM> is also defined, which can be used in the
-generic portion of Proof General to set and retrieve the value for the current p.a.
+generic portion of Proof General to access the value for the current prover.
 Arguments as for `defcustom', which see.
 
 Usage: (defpgcustom SYM &rest ARGS)."
@@ -248,6 +250,97 @@ Usage: (defpgdefault SYM VALUE)"
   `(defun ,(proof-ass-symv name) ,arglist
      ,@args))
 
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
+;; Prover-assistant specific customizations 
+;; which are recorded in `proof-assistant-settings'
+;;
+
+;;; autoload for compiled version: used in macro proof-defpacustom
+;;;###autoload
+(defun proof-defpacustom-fn (name val args)
+  "As for macro `defpacustom' but evaluating arguments."
+  (let (newargs setting evalform type descr)
+    (while args
+      (cond
+       ((eq (car args) :setting)
+	(setq setting (cadr args))
+	(setq args (cdr args)))
+       ((eq (car args) :eval)
+	(setq evalform (cadr args))
+	(setq args (cdr args)))
+       ((eq (car args) :pgipcmd)
+	;; Construct a function which yields a PGIP string
+	(setq setting `(lambda (x)
+			  (pg-pgip-string-of-command (proof-assistant-format ,(cadr args) x))))
+	(setq args (cdr args)))
+       ((eq (car args) :pggroup)
+	;; use the group as a prefix to the name, and set a pggroup property on it
+	(setq name (intern (concat (downcase (cadr args)) ":" (symbol-name name))))
+	(put name 'pggroup (cadr args))
+	(setq args (cdr args)))
+       ((eq (car args) :type)
+	(setq type (cadr args))
+	(setq args (cdr args))
+	(setq newargs (cons type (cons :type newargs))))
+       (t
+	(setq newargs (cons (car args) newargs))))
+      (setq args (cdr args)))
+    (setq newargs (reverse newargs))
+    (setq descr (car-safe newargs))
+    (unless (and type
+		  (or (eq (eval type) 'boolean)
+		      (eq (eval type) 'integer)
+		      (eq (eval type) 'string)))
+      (error "defpacustom: missing :type keyword or wrong :type value"))
+    ;; Debug message in case a defpacustom is repeated.
+    ;; NB: this *may* happen dynamically, but shouldn't: if the
+    ;; interface queries the prover for the settings it supports,
+    ;; then the internal list should be cleared first.
+    ;; FIXME: for now, we support redefinitions, by calling
+    ;; pg-custom-undeclare-variable.
+    (if (assoc name proof-assistant-settings)
+	(progn
+	  (proof-debug "defpacustom: Proof assistant setting %s re-defined!"
+		       name)
+	  (undefpgcustom name)))
+    (eval
+     `(defpgcustom ,name ,val
+	,@newargs
+	:set 'proof-set-value
+	:group 'proof-assistant-setting))
+    (cond
+     (evalform
+      (eval
+       `(defpgfun ,name ()
+	  ,evalform)))
+     (setting
+      (eval
+       `(defpgfun ,name ()
+	  (proof-assistant-invisible-command-ifposs
+	   (proof-assistant-settings-cmd (quote ,name)))))))
+    (setq proof-assistant-settings
+	  (cons (list name setting (eval type) descr)
+		(assq-delete-all name proof-assistant-settings)))))
+
+;;;###autoload
+(defmacro defpacustom (name val &rest args)
+  "Define a setting NAME for the current proof assitant, default VAL.
+NAME can correspond to some internal setting, flag, etc, for the
+proof assistant, in which case a :setting and :type value should be provided.
+The :type of NAME should be one of 'integer, 'boolean, 'string.
+The customization variable is automatically in group `proof-assistant-setting'.
+The function `proof-assistant-format' is used to format VAL.
+If NAME corresponds instead to a PG internal setting, then a form :eval to
+evaluate can be provided instead."
+  (eval-when-compile
+    (if (boundp 'proof-assistant-symbol)
+	;; declare variable to compiler to prevent warnings
+	(eval `(defvar ,(proof-ass-sym name) nil "Dummy for compilation."))))
+  `(proof-defpacustom-fn (quote ,name) (quote ,val) (quote ,args)))
+
+
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
 ;; Evaluation once proof assistant is known
@@ -457,17 +550,6 @@ No effect if buffer is dead."
 	(if proof-delete-empty-windows
 	    (delete-windows-on buffer t)))))
 
-(defun proof-message (&rest args)
-  "Issue the message ARGS in the response buffer and display it."
-  (pg-response-display-with-face (apply 'concat args))
-  (proof-display-and-keep-buffer proof-response-buffer))
-
-(defun proof-warning (&rest args)
-  "Issue the warning ARGS in the response buffer and display it.
-The warning is coloured with proof-warning-face."
-  (pg-response-display-with-face (apply 'concat args) 'proof-warning-face)
-  (proof-display-and-keep-buffer proof-response-buffer))
-
 (defun pg-internal-warning (message &rest args)
   "Display internal warning MESSAGE with ARGS as for format."
   (let ((formatted (apply 'format message args)))