Support custom syntactic fontification. Split out pa macros.

1 files changed, 11 insertions, 228 deletions

diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index 908bcf70..209f2747 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -14,16 +14,8 @@
 ;; Compilation note: see etc/development-tips.txt
 ;;
 
-(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
-
+;;; Code:
 
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
 ;; Give Emacs version mismatch error here.
 ;;
@@ -49,8 +41,15 @@
    "Proof General was compiled for %s but running on %s: please run \"make clean; make\""
    pg-compiled-for (pg-emacs-version-cookie)))
 
-;;
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+
+(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
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -139,223 +138,6 @@ Return nil if not a script buffer or if no active scripting buffer."
 			     (buffer-file-name (current-buffer)))))
       (save-buffer)))
 
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;
-;; Macros for defining per-assistant customization settings.
-;;
-;; This new 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
-;; slightly more complicated, and less "object-oriented" than the
-;; previous approach.  It is also a big change to move all settings.
-;;
-;; NB: this mechanism is work in progress in 3.2.  It will
-;; be expanded, although we may leave most low-level
-;; settings to use the current mechanism.
-;;
-;; Notes:
-;;
-;; Two mechanisms for accessing generic vars:
-;;
-;; (proof-ass name)   or (proof-assistant-name)
-;;
-
-(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 <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)))))
-    (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 <PA>-SYM for the current proof assistant.
-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 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 <PA>-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 <PA>-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.
-    ;; 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
-;;
-
-(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))))
-
-
-
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
@@ -559,6 +341,7 @@ No effect if buffer is dead."
 	(display-warning 'proof-general formatted)
     (message formatted))))
 
+;;;###autoload
 (defun proof-debug (msg &rest args)
   "Issue the debugging message (format MSG ARGS) in the response buffer, display it.
 If proof-general-debug is nil, do nothing."