diff options
author | David Aspinall <da@inf.ed.ac.uk> | 2011-01-31 08:56:12 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 2011-01-31 08:56:12 +0000 |
commit | 17c414438339c4edc9fabc2a1f751ddbb1a685c6 (patch) | |
tree | 0fbc7cbbb2a886242ac7862f63f70ce457d280da | |
parent | e482a7dc259dc63c0404dd3c38649317524cd721 (diff) |
Improve handling of dynamic preferences. Addresses Trac #387.
-rw-r--r-- | generic/pg-pamacs.el | 62 | ||||
-rw-r--r-- | generic/pg-pgip.el | 3 | ||||
-rw-r--r-- | generic/proof-menu.el | 15 |
3 files changed, 56 insertions, 24 deletions
diff --git a/generic/pg-pamacs.el b/generic/pg-pamacs.el index a8e3f67c..798e1e78 100644 --- a/generic/pg-pamacs.el +++ b/generic/pg-pamacs.el @@ -1,6 +1,6 @@ ;;; pg-pamacs.el --- Macros for per-proof assistant configuration ;; -;; Copyright (C) 2010 LFCS Edinburgh, David Aspinall. +;; Copyright (C) 2010, 2011 LFCS Edinburgh, David Aspinall. ;; ;; Author: David Aspinall <da@longitude> ;; Keywords: internal @@ -101,8 +101,6 @@ 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 @@ -163,13 +161,16 @@ 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) + (put name 'pgdynamic (cadr args)) + (setq args (cdr args))) ((eq (car args) :type) (setq type (cadr args)) (if (eq (eval type) 'float) (setq type (quote 'number))) ; widget type for defcustom (setq args (cdr args)) (setq newargs (cons type (cons :type newargs)))) - (t + (t ; first element, description (setq newargs (cons (car args) newargs)))) (setq args (cdr args))) (setq newargs (reverse newargs)) @@ -180,15 +181,12 @@ Usage: (defpgdefault SYM VALUE)" (eq (eval type) 'number) (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))) + + ;; Error in case a defpacustom is repeated. + (when (assoc name proof-assistant-settings) + (error "defpacustom: Proof assistant setting %s re-defined!" + name)) + (eval `(defpgcustom ,name ,val ,@newargs @@ -210,14 +208,40 @@ Usage: (defpgdefault SYM VALUE)" ;;;###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, 'float, 'boolean, 'string. -The customization variable is automatically in group `proof-assistant-setting'. + "Define a setting NAME for the current proof assistant, default VAL. +Mainly intended for configuring settings of running provers, +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. + The function `proof-assistant-format' is used to format VAL. + +This macro invokes the standard Emacs `defcustom' macro, so this +also defines a customizable setting inside Emacs. The +customization variable is automatically in group +`proof-assistant-setting'. + If NAME corresponds instead to a PG internal setting, then a form :eval to -evaluate can be provided instead." +evaluate can be provided instead. + +Additional properties in the ARGS prop list may include: + + pggroup string A grouping name for the setting, in case there are many. + For example, \"Timing\", \"Tracing\", etc. Used + to generate sub-menus in the UI. + + pgipgcmd string Alternative to :setting. + Send a PGIP formatted command based on given string. + + 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 + 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 diff --git a/generic/pg-pgip.el b/generic/pg-pgip.el index 16a0a6bd..b188d978 100644 --- a/generic/pg-pgip.el +++ b/generic/pg-pgip.el @@ -193,7 +193,8 @@ Return a symbol representing the PGIP command processed, or nil." `(defpacustom ,symname ,default ,descr :type (quote ,type) :pggroup ,prefcat - :pgipcmd ,pgipcmd)))) + :pgipcmd ,pgipcmd + :pgdynamic t)))) (defun pg-pgip-process-prefval (node) ;; diff --git a/generic/proof-menu.el b/generic/proof-menu.el index 741fab64..5c0bfeda 100644 --- a/generic/proof-menu.el +++ b/generic/proof-menu.el @@ -1,6 +1,6 @@ ;;; proof-menu.el --- Menus, keymaps, misc commands for Proof General ;; -;; Copyright (C) 2000,2001,2009,2010 LFCS Edinburgh. +;; Copyright (C) 2000,2001,2009,2010,2011 LFCS Edinburgh. ;; Authors: David Aspinall ;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;; @@ -920,9 +920,16 @@ KEY is the optional key binding." ))) (defun proof-maybe-askprefs () - "If `proof-use-pgip-askprefs' is non-nil, try to issue <askprefs>." - (if (and proof-use-pgip-askprefs proof-shell-issue-pgip-cmd) - (pg-pgip-askprefs))) + "If `proof-use-pgip-askprefs' is non-nil, try to issue <askprefs>. +This will configure dynamic settings used in the current prover session +and extend `proof-assistant-settings'. +We first clear the dynamic settings from `proof-assistant-settings'." + (when (and proof-use-pgip-askprefs proof-shell-issue-pgip-cmd) + (dolist (setting proof-assistant-settings) + (let ((name (car setting))) + (if (get name 'pgdynamic) + (undefpgcustom name)))) + (pg-pgip-askprefs))) (defun proof-assistant-settings-cmd (setting) |