From 4878ed1c9a0f269494ef22cff2bfb40bec1b69dc Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Wed, 11 Aug 2010 16:56:30 +0000 Subject: Support custom syntactic fontification. Split out pa macros. --- generic/pg-pamacs.el | 227 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 227 insertions(+) create mode 100644 generic/pg-pamacs.el (limited to 'generic/pg-pamacs.el') diff --git a/generic/pg-pamacs.el b/generic/pg-pamacs.el new file mode 100644 index 00000000..87f54cfd --- /dev/null +++ b/generic/pg-pamacs.el @@ -0,0 +1,227 @@ +;;; pg-pamacs.el --- Macros for per-proof assistant configuration +;; +;; Copyright (C) 2010 LFCS Edinburgh, David Aspinall. +;; +;; Author: David Aspinall +;; Keywords: internal + +;;; Commentary: +;; +;; Macros for defining per-assistant customization settings. +;; +;; This mechanism is an improved way to handle per-assistant settings. +;; Instead of declaring a variable "proof-assistant-web-page" and +;; duplicating it in the prover specific code to make the generic +;; setting, we automatically declare "isabelle-web-page", +;; "coq-web-page", etc, using these macros. +;; +;; The advantage of this is that people's save settings will work +;; properly, and that it will become more possible to use more than +;; one instance of PG at a time. The disadvantage is that it is more +;; complicated, and less "object-oriented" than the previous approach. +;; +;; There are two mechanisms for accessing generic vars: +;; +;; (proof-ass name) or (proof-assistant-name) +;; +;; +;; Developer's note: This code was previously in proof-utils.el. +;; + +(require 'proof-site) ; proof-assitant-symbol +(require 'proof-compat) ; pg-custom-undeclare-variable +(require 'proof-autoloads) ; proof-debug + +;;; Code: + + +(defmacro proof-ass-sym (sym) + "Return the symbol for SYM for the current prover. SYM not evaluated. +This macro should only be called once a specific prover is known." + `(intern (concat (symbol-name proof-assistant-symbol) "-" + (symbol-name ',sym)))) + +(defmacro proof-ass-symv (sym) + "Return the symbol for SYM for the current prover. SYM evaluated. +This macro should only be invoked once a specific prover is engaged." + `(intern (concat (symbol-name proof-assistant-symbol) "-" + (symbol-name ,sym)))) + +(defmacro proof-ass (sym) + "Return the value for SYM for the current prover. +This macro should only be invoked once a specific prover is engaged." + `(symbol-value (intern (concat (symbol-name proof-assistant-symbol) "-" + (symbol-name ',sym))))) + +(defun proof-defpgcustom-fn (sym args) + "Define a new customization variable -sym for current proof assistant. +Helper for macro `defpgcustom'." + (let ((specific-var (proof-ass-symv sym)) + (generic-var (intern (concat "proof-assistant-" (symbol-name sym))))) + (eval + `(defcustom ,specific-var + ,@args + ;; We could grab :group from @args and prefix it. + :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. + (eval + `(defun ,generic-var (&optional newval) + ,(concat "Set or get value of " (symbol-name sym) + " for current proof assistant. +If NEWVAL is present, set the variable, otherwise return its current value.") + (if newval + (setq ,specific-var newval) + ,specific-var))))) + +(defun undefpgcustom (sym) + (let ((specific-var (proof-ass-symv sym)) + (generic-var (intern (concat "proof-assistant-" (symbol-name sym))))) + (pg-custom-undeclare-variable specific-var) + (fmakunbound generic-var))) + +(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 access the value for the current prover. +Arguments as for `defcustom', which see. + +Usage: (defpgcustom SYM &rest ARGS)." + `(proof-defpgcustom-fn (quote ,sym) (quote ,args))) + + + +(defun proof-defpgdefault-fn (sym value) + "Helper for `defpgdefault', which see. SYM and VALUE are evaluated." + ;; NB: we need this because nothing in customize library seems to do + ;; the right thing. + (let ((symbol (proof-ass-symv sym))) + (set-default symbol + (cond + ;; Use saved value if it's set + ((get symbol 'saved-value) + (car (get symbol 'saved-value))) + ;; Otherwise override old default with new one + (t + value))))) + +(defmacro defpgdefault (sym value) + "Set default for the proof assistant specific variable -SYM to VALUE. +This should be used in prover-specific code to alter the default values +for prover specific settings. + +Usage: (defpgdefault SYM VALUE)" + `(proof-defpgdefault-fn (quote ,sym) ,value)) + +;; +;; Make a function named for the current proof assistant. +;; +(defmacro defpgfun (name arglist &rest args) + "Define function -SYM as for defun." + `(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. + (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 +;; + +(defmacro proof-eval-when-ready-for-assistant (&rest body) + "Evaluate BODY once the proof assistant is determined (possibly now)." + `(if (and (boundp 'proof-assistant-symbol) proof-assistant-symbol) + (progn ,@body) + (add-hook 'proof-ready-for-assistant-hook (lambda () ,@body)))) + + + +(provide 'pg-pamacs) +;;; pg-pamacs.el ends here -- cgit v1.2.3