From f9ba1c4e0cd55f068986419fe02d81b4258e3102 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Fri, 12 May 2000 17:06:16 +0000 Subject: Added proof-defassfun. Comments --- generic/proof-config.el | 18 ++++++++++++++---- 1 file changed, 14 insertions(+), 4 deletions(-) (limited to 'generic') diff --git a/generic/proof-config.el b/generic/proof-config.el index 72a229a5..36fcefb5 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -1873,15 +1873,14 @@ X-Symbol support is deactivated." ;; them all prover-specific automatically. Then people's save ;; settings would work, and we could remove all the "mirror" settings. ;; -;; NB: this section is work in progress +;; NB: this section is work in progress for 3.2, probably +;; to be moved to proof-utils ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; Macros ;; - - (defun proof-ass-symv (sym) "Return the symbol for SYM for the current prover. SYM is evaluated." (intern (concat (symbol-name proof-assistant-symbol) "-" @@ -1905,6 +1904,9 @@ Helper for macro `proof-defasscustom'." :group ,(quote proof-assistant-internals-cusgrp))) ;; For functions, we could simply use defalias. Unfortunately there ;; is nothing similar for values, so we define a new set/get function. + ;; FIXME: consider removing this code. Maybe we only need to read + ;; proof-assistant specific settings, not set them. That is the + ;; job of proof-assistant specific code, not generic code! (eval `(defun ,generic-var (&optional newval) ,(concat "Set or get value of " (symbol-name sym) " for current proof assistant. @@ -1946,7 +1948,15 @@ for prover specific settings." (defmacro proof-defass-default (sym value) `(proof-defass-default-fn (quote ,sym) ,value)) - + +;; +;; Make a function named for the current proof assistant. +;; +(defmacro proof-defassfun (name arglist &rest args) + "Define function -SYM as for defun." + `(defun ,(proof-ass-symv name) ,arglist + ,@args)) + ;; End macros -- cgit v1.2.3