From fa5ab22e50afb88abc34258679990abfea4c19bd Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Thu, 10 Sep 2009 08:49:46 +0000 Subject: Move defpacustom here. Move message functions to proof-shell. Fix requires. --- generic/proof-utils.el | 114 ++++++++++++++++++++++++++++++++++++++++++------- 1 file changed, 98 insertions(+), 16 deletions(-) (limited to 'generic/proof-utils.el') 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 -SYM for the current proof assistant. The function proof-assistant- 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))) -- cgit v1.2.3