Support custom syntactic fontification. Split out pa macros.

6 files changed, 337 insertions, 310 deletions

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 <da@longitude>
+;; 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 <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.
+    (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
diff --git a/generic/proof-autoloads.el b/generic/proof-autoloads.el
index 23b816e0..96299c26 100644
--- a/generic/proof-autoloads.el
+++ b/generic/proof-autoloads.el
@@ -169,7 +169,7 @@ This mode is only useful with a font which can display the maths repertoire.
 ;;;***
 
 ;;;### (autoloads (proof-associated-windows proof-associated-buffers)
-;;;;;;  "pg-assoc" "pg-assoc.el" (19121 59721))
+;;;;;;  "pg-assoc" "pg-assoc.el" (19550 46151))
 ;;; Generated autoloads from pg-assoc.el
 
 (autoload 'proof-associated-buffers "pg-assoc" "\
@@ -198,23 +198,46 @@ Initialise the goals buffer after the child has been configured.
 ;;;***
 
 ;;;### (autoloads (pg-movie-export-from pg-movie-export) "pg-movie"
-;;;;;;  "pg-movie.el" (19544 3005))
+;;;;;;  "pg-movie.el" (19550 46151))
 ;;; Generated autoloads from pg-movie.el
 
 (autoload 'pg-movie-export "pg-movie" "\
-Not documented
+Export the movie file from the current script buffer.
 
 \(fn)" t nil)
 
 (autoload 'pg-movie-export-from "pg-movie" "\
-Not documented
+Export the movie file that results from processing SCRIPT.
 
-\(fn SCRIPT)" nil nil)
+\(fn SCRIPT)" t nil)
+
+;;;***
+
+;;;### (autoloads (defpacustom proof-defpacustom-fn) "pg-pamacs"
+;;;;;;  "pg-pamacs.el" (19554 53996))
+;;; Generated autoloads from pg-pamacs.el
+
+(autoload 'proof-defpacustom-fn "pg-pamacs" "\
+As for macro `defpacustom' but evaluating arguments.
+
+\(fn NAME VAL ARGS)" nil nil)
+
+(autoload 'defpacustom "pg-pamacs" "\
+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.
+
+\(fn NAME VAL &rest ARGS)" nil (quote macro))
 
 ;;;***
 
 ;;;### (autoloads (pg-pgip-askprefs pg-pgip-maybe-askpgip pg-pgip-process-packet)
-;;;;;;  "pg-pgip" "pg-pgip.el" (19122 39720))
+;;;;;;  "pg-pgip" "pg-pgip.el" (19550 46151))
 ;;; Generated autoloads from pg-pgip.el
 
 (autoload 'pg-pgip-process-packet "pg-pgip" "\
@@ -238,7 +261,7 @@ Send an <askprefs> message to the prover.
 ;;;### (autoloads (pg-response-has-error-location proof-next-error
 ;;;;;;  pg-response-message pg-response-display-with-face pg-response-maybe-erase
 ;;;;;;  proof-response-config-done proof-response-mode) "pg-response"
-;;;;;;  "pg-response.el" (19542 60238))
+;;;;;;  "pg-response.el" (19550 46151))
 ;;; Generated autoloads from pg-response.el
 
 (autoload 'proof-response-mode "pg-response" "\
@@ -252,12 +275,12 @@ Complete initialisation of a response-mode derived buffer.
 \(fn)" nil nil)
 
 (autoload 'pg-response-maybe-erase "pg-response" "\
-Erase the response buffer according to pg-response-erase-flag.
+Erase the response buffer according to `pg-response-erase-flag'.
 ERASE-NEXT-TIME is the new value for the flag.
-If CLEAN-WINDOWS is set, use proof-clean-buffer to do the erasing.
-If FORCE, override pg-response-erase-flag.
+If CLEAN-WINDOWS is set, use `proof-clean-buffer' to do the erasing.
+If FORCE, override `pg-response-erase-flag'.
 
-If the user option proof-tidy-response is nil, then
+If the user option `proof-tidy-response' is nil, then
 the buffer is only cleared when FORCE is set.
 
 No effect if there is no response buffer currently.
@@ -294,27 +317,6 @@ See `pg-next-error-regexp'.
 
 ;;;***
 
-;;;### (autoloads (pg-defthymode) "pg-thymodes" "pg-thymodes.el"
-;;;;;;  (19108 51621))
-;;; Generated autoloads from pg-thymodes.el
-
-(autoload (quote pg-defthymode) "pg-thymodes" "\
-Define a Proof General mode for theory files.
-Mode name is SYM-mode, named NAMED.  BODY is the body of a setq and
-can define a number of variables for the mode, viz:
-
-  SYM-<font-lock-keywords>      (value for font-lock-keywords)
-  SYM-<syntax-table-entries>	(list of pairs: used for modify-syntax-entry calls)
-  SYM-<menu>			(menu for the mode, arg of easy-menu-define)
-  SYM-<parent-mode>		(defaults to fundamental-mode)
-  SYM-<filename-regexp>	        (regexp matching filenames for auto-mode-alist)
-
-All of these settings are optional.
-
-\(fn SYM NAME &rest BODY)" nil (quote macro))
-
-;;;***
-
 ;;;### (autoloads (pg-clear-input-ring pg-remove-from-input-history
 ;;;;;;  pg-add-to-input-history pg-next-matching-input-from-input
 ;;;;;;  pg-previous-matching-input-from-input proof-imenu-enable
@@ -322,7 +324,7 @@ All of these settings are optional.
 ;;;;;;  pg-response-buffers-hint pg-slow-fontify-tracing-hint proof-electric-terminator-enable
 ;;;;;;  proof-define-assistant-command-witharg proof-define-assistant-command
 ;;;;;;  proof-goto-point proof-script-new-command-advance) "pg-user"
-;;;;;;  "pg-user.el" (19543 7684))
+;;;;;;  "pg-user.el" (19550 46151))
 ;;; Generated autoloads from pg-user.el
 
 (autoload 'proof-script-new-command-advance "pg-user" "\
@@ -440,7 +442,7 @@ Parse string in ARG, same as pg-xml-parse-buffer.
 ;;;***
 
 ;;;### (autoloads (proof-dependency-in-span-context-menu proof-depends-process-dependencies)
-;;;;;;  "proof-depends" "proof-depends.el" (19222 64809))
+;;;;;;  "proof-depends" "proof-depends.el" (19550 46151))
 ;;; Generated autoloads from proof-depends.el
 
 (autoload 'proof-depends-process-dependencies "proof-depends" "\
@@ -451,7 +453,7 @@ Called from `proof-done-advancing' when a save is processed and
 \(fn NAME GSPAN)" nil nil)
 
 (autoload 'proof-dependency-in-span-context-menu "proof-depends" "\
-Make a portion of a context-sensitive menu showing proof dependencies.
+Make some menu entries showing proof dependencies of SPAN.
 
 \(fn SPAN)" nil nil)
 
@@ -471,7 +473,7 @@ the `proof-assistant-table', which see.
 ;;;***
 
 ;;;### (autoloads (proof-indent-line) "proof-indent" "proof-indent.el"
-;;;;;;  (19220 21213))
+;;;;;;  (19550 46151))
 ;;; Generated autoloads from proof-indent.el
 
 (autoload 'proof-indent-line "proof-indent" "\
@@ -482,7 +484,7 @@ Indent current line of proof script, if indentation enabled.
 ;;;***
 
 ;;;### (autoloads (proof-maths-menu-enable proof-maths-menu-set-global)
-;;;;;;  "proof-maths-menu" "proof-maths-menu.el" (19122 39720))
+;;;;;;  "proof-maths-menu" "proof-maths-menu.el" (19550 46151))
 ;;; Generated autoloads from proof-maths-menu.el
 
 (autoload 'proof-maths-menu-set-global "proof-maths-menu" "\
@@ -503,8 +505,8 @@ in future if we have just activated it for this buffer.
 ;;;***
 
 ;;;### (autoloads (proof-aux-menu proof-menu-define-specific proof-menu-define-main
-;;;;;;  proof-menu-define-keys) "proof-menu" "proof-menu.el" (19223
-;;;;;;  1323))
+;;;;;;  proof-menu-define-keys) "proof-menu" "proof-menu.el" (19550
+;;;;;;  46151))
 ;;; Generated autoloads from proof-menu.el
 
 (autoload 'proof-menu-define-keys "proof-menu" "\
@@ -530,7 +532,7 @@ Construct and return PG auxiliary menu used in non-scripting buffers.
 ;;;***
 
 ;;;### (autoloads (proof-mmm-enable proof-mmm-set-global) "proof-mmm"
-;;;;;;  "proof-mmm.el" (19121 59722))
+;;;;;;  "proof-mmm.el" (19550 46151))
 ;;; Generated autoloads from proof-mmm.el
 
 (autoload 'proof-mmm-set-global "proof-mmm" "\
@@ -553,7 +555,7 @@ in future if we have just activated it for this buffer.
 ;;;;;;  proof-insert-pbp-command proof-register-possibly-new-processed-file
 ;;;;;;  pg-set-span-helphighlights proof-locked-region-empty-p proof-locked-region-full-p
 ;;;;;;  proof-unprocessed-begin proof-colour-locked) "proof-script"
-;;;;;;  "proof-script.el" (19543 20729))
+;;;;;;  "proof-script.el" (19554 53098))
 ;;; Generated autoloads from proof-script.el
 
 (autoload 'proof-colour-locked "proof-script" "\
@@ -637,7 +639,7 @@ finish setup which depends on specific proof assistant configuration.
 ;;;;;;  proof-shell-invisible-cmd-get-result proof-shell-invisible-command
 ;;;;;;  proof-shell-wait proof-extend-queue proof-start-queue proof-shell-insert
 ;;;;;;  proof-shell-available-p proof-shell-ready-prover) "proof-shell"
-;;;;;;  "proof-shell.el" (19543 16432))
+;;;;;;  "proof-shell.el" (19550 46151))
 ;;; Generated autoloads from proof-shell.el
 
 (autoload 'proof-shell-ready-prover "proof-shell" "\
@@ -705,14 +707,14 @@ Needed between sequences of commands to maintain synchronization,
 because Proof General does not allow for the action list to be extended
 in some cases.   May be called by `proof-shell-invisible-command'.
 
-\(fn)" nil nil)
+\(fn &optional INTERRUPT-ON-INPUT)" nil nil)
 
 (autoload 'proof-shell-invisible-command "proof-shell" "\
 Send CMD to the proof process.
 The CMD is `invisible' in the sense that it is not recorded in buffer.
 CMD may be a string or a string-yielding expression.
 
-Automatically add proof-terminal-char if necessary, examining
+Automatically add `proof-terminal-char' if necessary, examining
 `proof-shell-no-auto-terminate-commands'.
 
 By default, let the command be processed asynchronously.
@@ -725,7 +727,7 @@ INVISIBLECALLBACK will be invoked after the command has finished,
 if it is set.  It should probably run the hook variables
 `proof-state-change-hook'.
 
-If NOERROR is set, surpress usual error action.
+FLAGS are put onto the If NOERROR is set, surpress usual error action.
 
 \(fn CMD &optional WAIT INVISIBLECALLBACK &rest FLAGS)" nil nil)
 
@@ -758,7 +760,7 @@ processing.
 ;;;***
 
 ;;;### (autoloads (proof-ready-for-assistant) "proof-site" "proof-site.el"
-;;;;;;  (19542 60238))
+;;;;;;  (19554 54083))
 ;;; Generated autoloads from proof-site.el
 
 (autoload 'proof-ready-for-assistant "proof-site" "\
@@ -770,16 +772,16 @@ If ASSISTANT-NAME is omitted, look up in `proof-assistant-table'.
 ;;;***
 
 ;;;### (autoloads (proof-splash-message proof-splash-display-screen)
-;;;;;;  "proof-splash" "proof-splash.el" (19109 19687))
+;;;;;;  "proof-splash" "proof-splash.el" (19550 46151))
 ;;; Generated autoloads from proof-splash.el
 
-(autoload (quote proof-splash-display-screen) "proof-splash" "\
+(autoload 'proof-splash-display-screen "proof-splash" "\
 Save window config and display Proof General splash screen.
 If TIMEOUT is non-nil, arrange for a time-out to occur outside this function.
 
 \(fn &optional TIMEOUT)" t nil)
 
-(autoload (quote proof-splash-message) "proof-splash" "\
+(autoload 'proof-splash-message "proof-splash" "\
 Make sure the user gets welcomed one way or another.
 
 \(fn)" t nil)
@@ -787,9 +789,12 @@ Make sure the user gets welcomed one way or another.
 ;;;***
 
 ;;;### (autoloads (proof-format) "proof-syntax" "proof-syntax.el"
-;;;;;;  (19220 59810))
+;;;;;;  (19554 53840))
 ;;; Generated autoloads from proof-syntax.el
 
+(defsubst proof-replace-regexp-in-string (regexp rep string) "\
+Like replace-regexp-in-string, but set case-fold-search to proof-case-fold-search." (let ((case-fold-search proof-case-fold-search)) (replace-regexp-in-string regexp rep string)))
+
 (autoload 'proof-format "proof-syntax" "\
 Format a string by matching regexps in ALIST against STRING.
 ALIST contains (REGEXP . REPLACEMENT) pairs where REPLACEMENT
@@ -800,7 +805,7 @@ may be a string or sexp evaluated to get a string.
 ;;;***
 
 ;;;### (autoloads (proof-toolbar-scripting-menu proof-toolbar-setup)
-;;;;;;  "proof-toolbar" "proof-toolbar.el" (19121 59722))
+;;;;;;  "proof-toolbar" "proof-toolbar.el" (19550 46151))
 ;;; Generated autoloads from proof-toolbar.el
 
 (autoload 'proof-toolbar-setup "proof-toolbar" "\
@@ -847,26 +852,15 @@ is changed.
 
 ;;;***
 
-;;;### (autoloads (defpacustom proof-defpacustom-fn) "proof-utils"
-;;;;;;  "proof-utils.el" (19135 42885))
+;;;### (autoloads (proof-debug) "proof-utils" "proof-utils.el" (19554
+;;;;;;  54161))
 ;;; Generated autoloads from proof-utils.el
 
-(autoload 'proof-defpacustom-fn "proof-utils" "\
-As for macro `defpacustom' but evaluating arguments.
-
-\(fn NAME VAL ARGS)" nil nil)
+(autoload 'proof-debug "proof-utils" "\
+Issue the debugging message (format MSG ARGS) in the response buffer, display it.
+If proof-general-debug is nil, do nothing.
 
-(autoload 'defpacustom "proof-utils" "\
-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.
-
-\(fn NAME VAL &rest ARGS)" nil (quote macro))
+\(fn MSG &rest ARGS)" nil nil)
 
 ;;;***
 
@@ -929,7 +923,7 @@ in your emacs font.
 ;;;***
 
 ;;;### (autoloads (unicode-tokens-encode-str) "unicode-tokens" "../lib/unicode-tokens.el"
-;;;;;;  (19496 21913))
+;;;;;;  (19551 10455))
 ;;; Generated autoloads from ../lib/unicode-tokens.el
 
 (autoload 'unicode-tokens-encode-str "unicode-tokens" "\
@@ -943,7 +937,7 @@ Return a unicode encoded version presentation of STR.
 ;;;;;;  "../lib/pg-fontsets.el" "../lib/proof-compat.el" "../lib/span.el"
 ;;;;;;  "pg-autotest.el" "pg-custom.el" "pg-pbrpm.el" "pg-vars.el"
 ;;;;;;  "proof-auxmodes.el" "proof-config.el" "proof-faces.el" "proof-useropts.el"
-;;;;;;  "proof.el") (19544 3030 500218))
+;;;;;;  "proof.el") (19554 54164 534243))
 
 ;;;***
 
diff --git a/generic/proof-faces.el b/generic/proof-faces.el
index 7fe80ea7..c64aad7a 100644
--- a/generic/proof-faces.el
+++ b/generic/proof-faces.el
@@ -141,7 +141,7 @@ Warning messages can come from proof assistant or from Proof General itself."
 
 (defface proof-boring-face
   (proof-face-specs
-   (:foreground "Gray65")
+   (:foreground "Gray85")
    (:background "Gray30")
    (:italic t))
   "*Face for boring text in proof assistant output."
diff --git a/generic/proof-script.el b/generic/proof-script.el
index bedfd68c..0939855a 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -2308,7 +2308,10 @@ mode features, but are only ever processed atomically by the proof
 assistant."
   (setq proof-script-buffer-file-name buffer-file-name)
 
-  (setq font-lock-defaults '(proof-script-font-lock-keywords))
+  (setq font-lock-defaults 
+	(list '(proof-script-font-lock-keywords)
+	      ;; see defadvice in proof-syntax 
+	      (fboundp (proof-ass-sym font-lock-fontify-syntactically-region))))
 
   ;; Has buffer already been processed?
   ;; NB: call to file-truename is needed for GNU Emacs which
diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el
index 4ca8b9fe..b44a5fa4 100644
--- a/generic/proof-syntax.el
+++ b/generic/proof-syntax.el
@@ -1,6 +1,6 @@
 ;; proof-syntax.el --- Functions for dealing with syntax
 ;;
-;; Copyright (C) 1997-2001 LFCS Edinburgh.
+;; Copyright (C) 1997-2001, 2010 LFCS Edinburgh.
 ;; Authors:   David Aspinall, Healfdene Goguen,
 ;;	      Thomas Kleymann, Dilip Sequiera
 ;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
@@ -11,6 +11,7 @@
 (require 'font-lock)
 (require 'proof-config)			; proof-case-fold-search
 (require 'proof-compat)			; proof-buffer-syntactic-context
+(require 'pg-pamacs)			; proof-ass-sym
 
 ;;; Code:
 
@@ -56,6 +57,7 @@ nil if a region cannot be found."
       ((case-fold-search proof-case-fold-search))
     (search-forward string bound noerror count)))
 
+;;;###autoload
 (defsubst proof-replace-regexp-in-string (regexp rep string)
   "Like replace-regexp-in-string, but set case-fold-search to proof-case-fold-search."
   (let ((case-fold-search proof-case-fold-search))
@@ -144,23 +146,41 @@ Default is comma separated, or SEPREGEXP if set."
 	  proof-id "\\)*"))
 
 
-;;
-;; A function to unfontify commas in declarations and definitions.
-;; Useful for provers which have declarations of the form x,y,z:Ty
-;; All that can be said for it is that the previous ways of doing
-;; this were even more bogus....
-;;
-
 (defun proof-zap-commas (limit)
   "Remove the face of all `,' from point to LIMIT.
-Meant to be used from `font-lock-keywords'."
-  (while (proof-search-forward "," limit t)
+Meant to be used from `font-lock-keywords' as a way
+to unfontify commas in declarations and definitions.
+Useful for provers which have declarations of the form x,y,z:Ty
+All that can be said for it is that the previous ways of doing
+this were even more bogus...."  
+(while (proof-search-forward "," limit t)
     (if (memq (get-text-property (1- (point)) 'face)
 	      '(proof-declaration-name-face
 		font-lock-variable-name-face
 		font-lock-function-name-face))
 	(put-text-property (1- (point)) (point) 'face nil))))
 
+
+;;
+;; Font lock: providing an alternative syntactic fontify
+;; region function.
+;; 
+;; The hook font-lock-fontify-region-function is tempting but not
+;; really a convenient place.  We just want to replace the syntactic
+;; fontification function.
+;;
+
+(eval-after-load "font-lock"
+'(progn
+(defadvice font-lock-fontify-keywords-region 
+  (before font-lock-fontify-keywords-advice (beg end loudly))
+  "Call proof assistant specific syntactic region fontify.
+If it's bound, we call <PA>-font-lock-fontify-syntactically-region."
+  (when (fboundp (proof-ass-sym font-lock-fontify-syntactically-region))
+    (funcall (proof-ass-sym font-lock-fontify-syntactically-region)
+	     beg end loudly)))
+(ad-activate 'font-lock-fontify-keywords-region)))
+
 ;;
 ;; Functions for doing something like "format" but with customizable
 ;; control characters.
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."