diff options
Diffstat (limited to 'generic/pg-pamacs.el')
| -rw-r--r-- | generic/pg-pamacs.el | 53 |
1 files changed, 29 insertions, 24 deletions
diff --git a/generic/pg-pamacs.el b/generic/pg-pamacs.el index 4958b360..1492e0ca 100644 --- a/generic/pg-pamacs.el +++ b/generic/pg-pamacs.el @@ -1,8 +1,16 @@ ;;; pg-pamacs.el --- Macros for per-proof assistant configuration -;; -;; Copyright (C) 2010, 2011 LFCS Edinburgh, David Aspinall. -;; + +;; This file is part of Proof General. + +;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh +;; Portions © Copyright 2003, 2012, 2014 Free Software Foundation, Inc. +;; Portions © Copyright 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel + ;; Author: David Aspinall <da@longitude> + ;; Keywords: internal ;;; Commentary: @@ -24,18 +32,17 @@ ;; ;; (proof-ass name) or (proof-assistant-name) ;; -;; + +;;; Code: (require 'proof-site) ; proof-assitant-symbol (require 'proof-compat) ; pg-custom-undeclare-variable (require 'proof-autoloads) ; proof-debug -;;; Code: - -(defmacro deflocal (var value &optional docstring) - "Define a buffer local variable VAR with default value VALUE." +(defmacro deflocal (var value &optional doc) + "Define a buffer local variable VAR with default value VALUE and docstring DOC." `(progn - (defvar ,var nil ,docstring) + (defvar ,var nil ,doc) (make-variable-buffer-local (quote ,var)) (setq-default ,var ,value))) @@ -72,13 +79,13 @@ This macro should only be invoked once a specific prover is engaged." (symbol-value pasym))))) (defun proof-defpgcustom-fn (sym args) - "Define a new customization variable <PA>-sym for current proof assistant. + "Define a new customization variable <PA>-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)))) - (newargs (if (member :group args) - args - (append (list :group + (newargs (if (member :group args) + args + (append (list :group proof-assistant-internals-cusgrp) args)))) (eval @@ -109,7 +116,7 @@ but which the user may require different values of across provers. The function proof-assistant-<SYM> is also defined, which can be used in the generic portion of Proof General to access the value for the current prover. -Arguments are as for `defcustom', which see. If a :group argument is +Arguments ARGS are as for `defcustom', which see. If a :group argument is not supplied, the setting will be added to the internal settings for the current prover (named <PA>-config)." `(proof-defpgcustom-fn (quote ,sym) (quote ,args))) @@ -155,6 +162,8 @@ Usage: (defpgdefault SYM VALUE)" ;;;###autoload (defun proof-defpacustom-fn (name val args) "As for macro `defpacustom' but evaluating arguments." + (unless (and proof-assistant (not (string= proof-assistant ""))) + (error "No proof assistant defined")) (let (newargs setting evalform type descr) (while args (cond @@ -174,7 +183,7 @@ Usage: (defpgdefault SYM VALUE)" (setq name (intern (concat (downcase (cadr args)) ":" (symbol-name name)))) (put name 'pggroup (cadr args)) (setq args (cdr args))) - ((eq (car args) :pgdynamic) + ((eq (car args) :pgdynamic) (put name 'pgdynamic (cadr args)) (setq args (cdr args))) ((eq (car args) :type) @@ -193,11 +202,11 @@ Usage: (defpgdefault SYM VALUE)" (eq (eval type) 'integer) (eq (eval type) 'number) (eq (eval type) 'string))) - (error "defpacustom: missing :type keyword or wrong :type value")) + (error "Macro defpacustom: missing :type keyword or wrong :type value")) ;; Error in case a defpacustom is repeated. (when (assq name proof-assistant-settings) - (error "defpacustom: Proof assistant setting %s re-defined!" + (error "Macro defpacustom: Proof assistant setting %s re-defined!" name)) (eval @@ -228,8 +237,8 @@ which can be changed by sending commands. In this case, NAME stands for the internal setting, flag, etc, for the proof assistant, and a :setting and :type value should be provided. The :type of NAME should be one of 'integer, 'float, -'boolean, 'string. Other types are not supported (see -`proof-menu-entry-for-setting'). They will yield an error when +'boolean, 'string. Other types are not supported (see +`proof-menu-entry-for-setting'). They will yield an error when constructing the proof assistant menu. The function `proof-assistant-format' is used to format VAL. @@ -253,14 +262,10 @@ Additional properties in the ARGS prop list may include: pgdynamic flag If flag is non-nil, this setting is a dynamic one that is particular to the running instance of the prover. - Automatically set by preferences configured from PGIP + Automatically set by preferences configured from PGIP askprefs message. This macro also extends the `proof-assistant-settings' list." - (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))) |