* coq-mode.el: New file to make coq-mode independent from PG

Move the part of coq.el that is not specific to ProofGeneral into coq-mode.el
to make `coq-mode` into a major mode that can work without PG.

* coq/coq-mode.el: New file, with code extracted from coq.el.
(coq-use-pg): New var.
(coq-near-comment-region): Complete rewrite.

* Makefile.devel (autoloads): Add `coq` to the scanned subdirectories.
* generic/proof-autoloads.el: Regenerate.

* generic/proof-site.el: Don't override pre-existing major-mode definitions.

* coq/coq-syntax.el (coq-init-syntax-table): Delete function.
Setup the syntax-table while loading coq-mode.el instead.

* coq/coq-system.el (coq-prog-name, get-coq-library-directory)
(coq-library-directory, coq-tags): Move to coq-mode.el.

* coq/coq.el: Set proof-assistant when loaded.
(coq-may-use-prettify, coq-outline-regexp)
(coq-outline-heading-end-regexp, coq-mode)
(coq-prettify-symbols-alist, coq-fill-paragraph-function)
(coq-adaptive-fill-function): Move to coq-mode.el.
(coq-shell-mode-syntax-table, coq-response-mode-syntax-table)
(coq-goals-mode-syntax-table): Just reuse the already setup
coq-mode-syntax-table...
(coq-shell-mode-config, coq-goals-mode-config, coq-response-config):
... instead of calling coq-init-syntax-table.
(coq-get-comment-region): Delete, not used any more.
(coq-pg-mode-map): New var.  Move top-level keymap setup here.
(coq-pg-setup): Rename from coq-mode-config.
Move all the non-PG specific settings to coq-mode.

* generic/proof-script.el (proof-mode): Simplify call to
proof-splash-message since it does the same extra tests internally.
(proof-config-done-related): Don't touch font-lock-defaults if the mode
doesn't provide any font-lock-defaults.

* isar/isar-syntax.el: Use lexical-binding.
(isar-font-lock-fontify-syntactically-region): Make it
callable from font0lock-keywords.
(isar-font-lock-keywords-1):
Call isar-font-lock-fontify-syntactically-region.

* generic/proof-syntax.el (font-lock-fontify-keywords-region):
Remove advice.
(proof-ids): Remove, unused.

* lib/bufhist.el (bufhist-erase-buffer):
Don't let-bind after-change-functions.

* generic/pg-pbrpm.el (pg-pbrpm-auto-select-around-point):
Fix one more left-over cl.el use.

* generic/proof-utils.el (proof-with-script-buffer): Add edebug spec.

7 files changed, 125 insertions, 91 deletions

diff --git a/generic/pg-pbrpm.el b/generic/pg-pbrpm.el
index b40cfff3..7a22e185 100644
--- a/generic/pg-pbrpm.el
+++ b/generic/pg-pbrpm.el
@@ -121,7 +121,7 @@ Matches the region to be returned.")
 ;	    (funcall 'proof-mode-for-shell) (funcall 'proof-mode))
 ; da: it's the name of a function, not fn itself. See pg-vars
 	(funcall proof-mode-for-script)
-	(add-hook 'after-change-functions 'pg-pbrpm-menu-change-hook nil t)
+	(add-hook 'after-change-functions #'pg-pbrpm-menu-change-hook nil t)
     (pg-pbrpm-erase-buffer-menu)))
   (set-buffer pg-pbrpm-buffer-menu))
 
@@ -425,7 +425,7 @@ If no match found, return the empty string."
       (cl-block 'loop
 	(while (< (point) pos)
 	  (unless (search-forward-regexp pg-pbrpm-auto-select-regexp nil t)
-	    (return-from 'loop ""))
+	    (cl-return-from 'loop ""))
 	  (if (and (<= (match-beginning 0) pos)
 		   (<= pos (match-end 0)))
 	      (cl-return-from 'loop (match-string 0))))
diff --git a/generic/proof-autoloads.el b/generic/proof-autoloads.el
index 5d2a18cd..302ad21e 100644
--- a/generic/proof-autoloads.el
+++ b/generic/proof-autoloads.el
@@ -23,8 +23,45 @@
 (provide 'proof-autoloads)
 
 
-;;;### (autoloads nil "../lib/bufhist" "../lib/bufhist.el" (23421
-;;;;;;  61555 968003 660000))
+;;;### (autoloads nil "../coq/coq" "../coq/coq.el" (23576 63508 474604
+;;;;;;  77000))
+;;; Generated autoloads from ../coq/coq.el
+
+(autoload 'coq-pg-setup "../coq/coq" "\
+
+
+\(fn)" nil nil)
+
+;;;***
+
+;;;### (autoloads nil "../coq/coq-autotest" "../coq/coq-autotest.el"
+;;;;;;  (23571 9656 963235 821000))
+;;; Generated autoloads from ../coq/coq-autotest.el
+
+(autoload 'coq-autotest "../coq/coq-autotest" "\
+
+
+\(fn)" t nil)
+
+;;;***
+
+;;;### (autoloads nil "../coq/coq-mode" "../coq/coq-mode.el" (23576
+;;;;;;  63738 715506 60000))
+;;; Generated autoloads from ../coq/coq-mode.el
+
+(add-to-list 'auto-mode-alist '("\\.v\\'" . coq-mode))
+
+(autoload 'coq-mode "../coq/coq-mode" "\
+Major mode for Coq scripts.
+
+\\{coq-mode-map}
+
+\(fn)" t nil)
+
+;;;***
+
+;;;### (autoloads nil "../lib/bufhist" "../lib/bufhist.el" (23576
+;;;;;;  10253 529610 111000))
 ;;; Generated autoloads from ../lib/bufhist.el
 
 (autoload 'bufhist-mode "../lib/bufhist" "\
@@ -55,8 +92,8 @@ Stop keeping ring history for current buffer.
 
 ;;;***
 
-;;;### (autoloads nil "../lib/holes" "../lib/holes.el" (23421 61555
-;;;;;;  968003 660000))
+;;;### (autoloads nil "../lib/holes" "../lib/holes.el" (23569 22945
+;;;;;;  718351 699000))
 ;;; Generated autoloads from ../lib/holes.el
 
 (autoload 'holes-set-make-active-hole "../lib/holes" "\
@@ -170,7 +207,7 @@ Insert S, expand it and replace #s and @{]s by holes.
 ;;;***
 
 ;;;### (autoloads nil "../lib/maths-menu" "../lib/maths-menu.el"
-;;;;;;  (23421 61555 968003 660000))
+;;;;;;  (23575 9250 536416 363000))
 ;;; Generated autoloads from ../lib/maths-menu.el
 
 (autoload 'maths-menu-mode "../lib/maths-menu" "\
@@ -183,8 +220,8 @@ This mode is only useful with a font which can display the maths repertoire.
 
 ;;;***
 
-;;;### (autoloads nil "pg-assoc" "pg-assoc.el" (23421 61555 964003
-;;;;;;  698000))
+;;;### (autoloads nil "pg-assoc" "pg-assoc.el" (23569 41729 794421
+;;;;;;  324000))
 ;;; Generated autoloads from pg-assoc.el
 
 (autoload 'proof-associated-buffers "pg-assoc" "\
@@ -208,8 +245,8 @@ Return the list of frames displaying at least one associated buffer.
 
 ;;;***
 
-;;;### (autoloads nil "../lib/pg-dev" "../lib/pg-dev.el" (23421 61555
-;;;;;;  968003 660000))
+;;;### (autoloads nil "../lib/pg-dev" "../lib/pg-dev.el" (23575 9250
+;;;;;;  536416 363000))
 ;;; Generated autoloads from ../lib/pg-dev.el
 
 (autoload 'profile-pg "../lib/pg-dev" "\
@@ -219,8 +256,8 @@ Configure Proof General for profiling.  Use \\[elp-results] to see results.
 
 ;;;***
 
-;;;### (autoloads nil "pg-goals" "pg-goals.el" (23421 61555 964003
-;;;;;;  698000))
+;;;### (autoloads nil "pg-goals" "pg-goals.el" (23575 9250 532416
+;;;;;;  428000))
 ;;; Generated autoloads from pg-goals.el
 
 (autoload 'proof-goals-config-done "pg-goals" "\
@@ -230,8 +267,8 @@ Initialise the goals buffer after the child has been configured.
 
 ;;;***
 
-;;;### (autoloads nil "pg-movie" "pg-movie.el" (23421 61555 964003
-;;;;;;  698000))
+;;;### (autoloads nil "pg-movie" "pg-movie.el" (23575 9223 344856
+;;;;;;  367000))
 ;;; Generated autoloads from pg-movie.el
 
 (autoload 'pg-movie-export "pg-movie" "\
@@ -253,8 +290,8 @@ Existing XML files are overwritten.
 
 ;;;***
 
-;;;### (autoloads nil "pg-pamacs" "pg-pamacs.el" (23421 61555 964003
-;;;;;;  698000))
+;;;### (autoloads nil "pg-pamacs" "pg-pamacs.el" (23576 62945 258166
+;;;;;;  137000))
 ;;; Generated autoloads from pg-pamacs.el
 
 (autoload 'proof-defpacustom-fn "pg-pamacs" "\
@@ -304,8 +341,7 @@ This macro also extends the `proof-assistant-settings' list.
 
 ;;;***
 
-;;;### (autoloads nil "pg-pgip" "pg-pgip.el" (23421 61555 964003
-;;;;;;  698000))
+;;;### (autoloads nil "pg-pgip" "pg-pgip.el" (23575 9250 532416 428000))
 ;;; Generated autoloads from pg-pgip.el
 
 (autoload 'pg-pgip-process-packet "pg-pgip" "\
@@ -326,8 +362,8 @@ Send an <askprefs> message to the prover.
 
 ;;;***
 
-;;;### (autoloads nil "pg-response" "pg-response.el" (23421 61555
-;;;;;;  964003 698000))
+;;;### (autoloads nil "pg-response" "pg-response.el" (23569 41729
+;;;;;;  794421 324000))
 ;;; Generated autoloads from pg-response.el
 
 (autoload 'proof-response-mode "pg-response" "\
@@ -396,8 +432,7 @@ See `pg-next-error-regexp'.
 
 ;;;***
 
-;;;### (autoloads nil "pg-user" "pg-user.el" (23421 61555 964003
-;;;;;;  698000))
+;;;### (autoloads nil "pg-user" "pg-user.el" (23571 8540 515663 574000))
 ;;; Generated autoloads from pg-user.el
 
 (autoload 'proof-script-new-command-advance "pg-user" "\
@@ -524,7 +559,7 @@ Enable or disable autosend behaviour.
 
 ;;;***
 
-;;;### (autoloads nil "pg-xml" "pg-xml.el" (23421 61555 964003 698000))
+;;;### (autoloads nil "pg-xml" "pg-xml.el" (23569 49953 922153 72000))
 ;;; Generated autoloads from pg-xml.el
 
 (autoload 'pg-xml-parse-string "pg-xml" "\
@@ -534,8 +569,8 @@ Parse string in ARG, same as pg-xml-parse-buffer.
 
 ;;;***
 
-;;;### (autoloads nil "proof-depends" "proof-depends.el" (23421 61555
-;;;;;;  964003 698000))
+;;;### (autoloads nil "proof-depends" "proof-depends.el" (23575 9250
+;;;;;;  532416 428000))
 ;;; Generated autoloads from proof-depends.el
 
 (autoload 'proof-depends-process-dependencies "proof-depends" "\
@@ -553,7 +588,7 @@ Make some menu entries showing proof dependencies of SPAN.
 ;;;***
 
 ;;;### (autoloads nil "proof-easy-config" "proof-easy-config.el"
-;;;;;;  (23421 61555 964003 698000))
+;;;;;;  (23548 4656 374888 298000))
 ;;; Generated autoloads from proof-easy-config.el
 
 (autoload 'proof-easy-config "proof-easy-config" "\
@@ -566,8 +601,8 @@ Additional arguments are taken into account as a setq BODY.
 
 ;;;***
 
-;;;### (autoloads nil "proof-indent" "proof-indent.el" (23421 34760
-;;;;;;  554828 678000))
+;;;### (autoloads nil "proof-indent" "proof-indent.el" (23548 4656
+;;;;;;  374888 298000))
 ;;; Generated autoloads from proof-indent.el
 
 (autoload 'proof-indent-line "proof-indent" "\
@@ -577,8 +612,8 @@ Indent current line of proof script, if indentation enabled.
 
 ;;;***
 
-;;;### (autoloads nil "proof-maths-menu" "proof-maths-menu.el" (23421
-;;;;;;  34760 554828 678000))
+;;;### (autoloads nil "proof-maths-menu" "proof-maths-menu.el" (23575
+;;;;;;  9250 532416 428000))
 ;;; Generated autoloads from proof-maths-menu.el
 
 (autoload 'proof-maths-menu-set-global "proof-maths-menu" "\
@@ -598,8 +633,8 @@ in future if we have just activated it for this buffer.
 
 ;;;***
 
-;;;### (autoloads nil "proof-menu" "proof-menu.el" (23421 61555 964003
-;;;;;;  698000))
+;;;### (autoloads nil "proof-menu" "proof-menu.el" (23576 8979 193466
+;;;;;;  461000))
 ;;; Generated autoloads from proof-menu.el
 
 (autoload 'proof-menu-define-keys "proof-menu" "\
@@ -624,8 +659,8 @@ Construct and return PG auxiliary menu used in non-scripting buffers.
 
 ;;;***
 
-;;;### (autoloads nil "proof-script" "proof-script.el" (23421 61555
-;;;;;;  964003 698000))
+;;;### (autoloads nil "proof-script" "proof-script.el" (23576 11228
+;;;;;;  990682 355000))
 ;;; Generated autoloads from proof-script.el
 
 (autoload 'proof-colour-locked "proof-script" "\
@@ -714,8 +749,8 @@ finish setup which depends on specific proof assistant configuration.
 
 ;;;***
 
-;;;### (autoloads nil "proof-shell" "proof-shell.el" (23421 61555
-;;;;;;  964003 698000))
+;;;### (autoloads nil "proof-shell" "proof-shell.el" (23575 9250
+;;;;;;  532416 428000))
 ;;; Generated autoloads from proof-shell.el
 
 (autoload 'proof-shell-ready-prover "proof-shell" "\
@@ -848,8 +883,8 @@ processing.
 
 ;;;***
 
-;;;### (autoloads nil "proof-site" "proof-site.el" (23421 61555 964003
-;;;;;;  698000))
+;;;### (autoloads nil "proof-site" "proof-site.el" (23576 62228 993634
+;;;;;;  734000))
 ;;; Generated autoloads from proof-site.el
 
 (autoload 'proof-ready-for-assistant "proof-site" "\
@@ -860,8 +895,8 @@ If ASSISTANT-NAME is omitted, look up in `proof-assistant-table'.
 
 ;;;***
 
-;;;### (autoloads nil "proof-splash" "proof-splash.el" (23421 61555
-;;;;;;  968003 660000))
+;;;### (autoloads nil "proof-splash" "proof-splash.el" (23576 11450
+;;;;;;  619317 210000))
 ;;; Generated autoloads from proof-splash.el
 
 (autoload 'proof-splash-display-screen "proof-splash" "\
@@ -879,8 +914,8 @@ Make sure the user gets welcomed one way or another.
 
 ;;;***
 
-;;;### (autoloads nil "proof-syntax" "proof-syntax.el" (23421 61555
-;;;;;;  968003 660000))
+;;;### (autoloads nil "proof-syntax" "proof-syntax.el" (23576 8794
+;;;;;;  396386 343000))
 ;;; Generated autoloads from proof-syntax.el
 
 (defsubst proof-replace-regexp-in-string (regexp rep string) "\
@@ -895,8 +930,8 @@ may be a string or sexp evaluated to get a string.
 
 ;;;***
 
-;;;### (autoloads nil "proof-toolbar" "proof-toolbar.el" (23421 34760
-;;;;;;  554828 678000))
+;;;### (autoloads nil "proof-toolbar" "proof-toolbar.el" (23548 4656
+;;;;;;  378888 227000))
 ;;; Generated autoloads from proof-toolbar.el
 
 (autoload 'proof-toolbar-setup "proof-toolbar" "\
@@ -915,7 +950,7 @@ Menu made from the Proof General toolbar commands.
 ;;;***
 
 ;;;### (autoloads nil "proof-unicode-tokens" "proof-unicode-tokens.el"
-;;;;;;  (23421 34760 554828 678000))
+;;;;;;  (23575 9250 536416 363000))
 ;;; Generated autoloads from proof-unicode-tokens.el
 
 (autoload 'proof-unicode-tokens-mode-if-enabled "proof-unicode-tokens" "\
@@ -942,8 +977,8 @@ is changed.
 
 ;;;***
 
-;;;### (autoloads nil "proof-utils" "proof-utils.el" (23421 61555
-;;;;;;  968003 660000))
+;;;### (autoloads nil "proof-utils" "proof-utils.el" (23576 62534
+;;;;;;  353957 67000))
 ;;; Generated autoloads from proof-utils.el
 
 (autoload 'proof-debug "proof-utils" "\
@@ -954,8 +989,8 @@ If flag `proof-general-debug' is nil, do nothing.
 
 ;;;***
 
-;;;### (autoloads nil "../lib/scomint" "../lib/scomint.el" (23421
-;;;;;;  61555 968003 660000))
+;;;### (autoloads nil "../lib/scomint" "../lib/scomint.el" (23575
+;;;;;;  9250 536416 363000))
 ;;; Generated autoloads from ../lib/scomint.el
 
 (autoload 'scomint-make-in-buffer "../lib/scomint" "\
@@ -987,7 +1022,7 @@ If PROGRAM is a string, the remaining SWITCHES are arguments to PROGRAM.
 ;;;***
 
 ;;;### (autoloads nil "../lib/texi-docstring-magic" "../lib/texi-docstring-magic.el"
-;;;;;;  (23421 61555 968003 660000))
+;;;;;;  (23575 9250 536416 363000))
 ;;; Generated autoloads from ../lib/texi-docstring-magic.el
 
 (autoload 'texi-docstring-magic "../lib/texi-docstring-magic" "\
@@ -1000,7 +1035,7 @@ With prefix arg, no errors on unknown symbols.  (This results in
 ;;;***
 
 ;;;### (autoloads nil "../lib/unicode-chars" "../lib/unicode-chars.el"
-;;;;;;  (23421 61555 968003 660000))
+;;;;;;  (23548 4656 382888 158000))
 ;;; Generated autoloads from ../lib/unicode-chars.el
 
 (autoload 'unicode-chars-list-chars "../lib/unicode-chars" "\
@@ -1013,7 +1048,7 @@ in your Emacs font.
 ;;;***
 
 ;;;### (autoloads nil "../lib/unicode-tokens" "../lib/unicode-tokens.el"
-;;;;;;  (23421 61555 968003 660000))
+;;;;;;  (23575 9250 540416 298000))
 ;;; Generated autoloads from ../lib/unicode-tokens.el
 
 (autoload 'unicode-tokens-encode-str "../lib/unicode-tokens" "\
@@ -1023,11 +1058,15 @@ Return a unicode encoded version presentation of STR.
 
 ;;;***
 
-;;;### (autoloads nil nil ("../lib/local-vars-list.el" "../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-tree.el" "proof-useropts.el"
-;;;;;;  "proof.el") (23421 61555 968003 660000))
+;;;### (autoloads nil nil ("../coq/coq-abbrev.el" "../coq/coq-compile-common.el"
+;;;;;;  "../coq/coq-db.el" "../coq/coq-indent.el" "../coq/coq-local-vars.el"
+;;;;;;  "../coq/coq-par-compile.el" "../coq/coq-par-test.el" "../coq/coq-seq-compile.el"
+;;;;;;  "../coq/coq-smie.el" "../coq/coq-syntax.el" "../coq/coq-system.el"
+;;;;;;  "../coq/coq-unicode-tokens.el" "../lib/local-vars-list.el"
+;;;;;;  "../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-tree.el"
+;;;;;;  "proof-useropts.el" "proof.el") (23577 1104 283265 664000))
 
 ;;;***
 
diff --git a/generic/proof-script.el b/generic/proof-script.el
index f8cf0cab..178477cf 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -2255,17 +2255,13 @@ query saves here."
 ;; Proof General scripting mode definition, part 1.
 ;;
 
-(defvar proof--splash-done nil)
-
 ;;;###autoload
 (define-derived-mode proof-mode fundamental-mode
   proof-general-name
   "Proof General major mode class for proof scripts.
 \\{proof-mode-map}"
 
-  (unless (or proof--splash-done noninteractive)
-    (setq proof--splash-done t)
-    (proof-splash-message))
+  (proof-splash-message)
 
   (setq proof-buffer-type 'script)
 
@@ -2374,10 +2370,11 @@ 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
-	(list '(proof-script-font-lock-keywords)
-	      ;; see defadvice in proof-syntax
-	      (fboundp (proof-ass-sym font-lock-fontify-syntactically-region))))
+  (when 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-site.el b/generic/proof-site.el
index fd48002f..7c185b2f 100644
--- a/generic/proof-site.el
+++ b/generic/proof-site.el
@@ -1,4 +1,4 @@
-;;; proof-site.el --- Loading stubs for Proof General.
+;;; proof-site.el --- Loading stubs for Proof General  -*- lexical-binding:t -*-
 
 ;; This file is part of Proof General.
 
@@ -361,10 +361,10 @@ the Lisp variable `proof-assistants', or the contents of `proof-assistant-table'
 	       (load-library ,elisp-file)
 	       (,proofgen-mode))))))
 
-	(setq auto-mode-alist
-	      (cons (cons regexp proofgen-mode) auto-mode-alist))
+	(add-to-list 'auto-mode-alist (cons regexp proofgen-mode))
 
-	(fset proofgen-mode mode-stub)
+        (unless (fboundp proofgen-mode)
+	  (fset proofgen-mode mode-stub))
 
 	(dolist (ext (nth 4 tableentry))
 	  (add-to-list 'completion-ignored-extensions ext))
diff --git a/generic/proof-splash.el b/generic/proof-splash.el
index 600e9b4e..bb8b5c0e 100644
--- a/generic/proof-splash.el
+++ b/generic/proof-splash.el
@@ -242,7 +242,7 @@ binding to remove this buffer."
 	(winconf   (current-window-configuration))
 	(curwin	   (get-buffer-window (current-buffer)))
 	(curfrm    (and curwin (window-frame curwin)))
-	(after-change-functions nil)	; no font-lock, thank-you.
+	(inhibit-modification-hooks t)	; no font-lock, thank-you.
 	 ;; NB: maybe leave next one in for frame-crazy folk
 	 ;;(pop-up-frames nil)		; display in the same frame.
 	(splashbuf (get-buffer-create proof-splash-welcome)))
@@ -275,7 +275,13 @@ binding to remove this buffer."
 	(progn
 	  ;; disable ordinary emacs splash
 	  (setq inhibit-startup-message t)
-	  (proof-splash-display-screen (not (called-interactively-p 'any))))
+          ;; Display the splash screen only after we're done setting things up,
+          ;; otherwise it can have undesired interference.
+          (run-with-timer
+           0 nil
+           `(lambda ()
+	      (proof-splash-display-screen
+               ,(not (called-interactively-p 'any))))))
       ;; Otherwise, a message
       (message "Welcome to %s Proof General!" proof-assistant))
     (setq proof-splash-seen t)))
diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el
index d494279a..2ba6b7b6 100644
--- a/generic/proof-syntax.el
+++ b/generic/proof-syntax.el
@@ -197,13 +197,6 @@ it calls `proof-looking-at-syntactic-context'."
 ;; For font-lock, we treat ,-separated identifiers as one identifier
 ;; and refontify commata using \{proof-zap-commas}.
 
-(defsubst proof-ids (proof-id &optional sepregexp)
-  "Generate a regular expression for separated lists of identifiers.
-Default is comma separated, or SEPREGEXP if set."
-  (concat proof-id "\\(\\s-*"   (or sepregexp ",") "\\s-*"
-	  proof-id "\\)*"))
-
-
 (defun proof-zap-commas (limit)
   "Remove the face of all `,' from point to LIMIT.
 Meant to be used from `font-lock-keywords' as a way
@@ -228,17 +221,15 @@ this were even more bogus...."
 ;; fontification function.
 ;;
 
-(eval-after-load "font-lock"
-'(progn
-(defadvice font-lock-fontify-keywords-region
-  (before font-lock-fontify-keywords-advice (beg end &optional loudly))
-  "Call proof assistant specific syntactic region fontify.
-If it's bound, we call <PA>-font-lock-fontify-syntactically-region."
-  (when (and proof-buffer-type
-	     (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)))
+;; (defadvice font-lock-fontify-keywords-region
+;;   (before font-lock-fontify-keywords-advice (beg end &optional loudly))
+;;   "Call proof assistant specific syntactic region fontify.
+;; If it's bound, we call <PA>-font-lock-fontify-syntactically-region."
+;;   (when (and proof-buffer-type
+;; 	     (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
diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index 4a15301a..39d1c22a 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -75,6 +75,7 @@
 (defmacro proof-with-script-buffer (&rest body)
   "Execute BODY in some script buffer: current buf, else ‘proof-script-buffer’.
 Return nil if not a script buffer or if no active scripting buffer."
+  (declare (debug t))
   `(cond
     ((eq proof-buffer-type 'script)
      (progn