* 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.

14 files changed, 479 insertions, 373 deletions

diff --git a/Makefile.devel b/Makefile.devel
index 603a43b4..d4339a46 100644
--- a/Makefile.devel
+++ b/Makefile.devel
@@ -246,7 +246,7 @@ distclean: devclean clean
 #
 autoloads: $(EL)
 	@echo "***** MAKING AUTOGENERATED AUTOLOADS  ****"
-	$(BATCHEMACS) -eval '(setq autoload-package-name "proof" generated-autoload-file "$(PWD)/generic/proof-autoloads.el")' -f batch-update-autoloads  generic/ lib/
+	$(BATCHEMACS) -eval '(setq autoload-package-name "proof" generated-autoload-file "$(PWD)/generic/proof-autoloads.el")' -f batch-update-autoloads  generic/ lib/ coq/
 
 ############################################################
 #
diff --git a/coq/coq-mode.el b/coq/coq-mode.el
new file mode 100644
index 00000000..f5d40027
--- /dev/null
+++ b/coq/coq-mode.el
@@ -0,0 +1,261 @@
+;;; coq-mode.el --- Major mode for Coq proof assistant  -*- lexical-binding:t -*-
+
+;; This file is part of Proof General.
+
+;; Portions © Copyright 1994-2012  David Aspinall and University of Edinburgh
+;; Portions © Copyright 2003, 2012, 2014, 2018  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
+
+;; Authors: Healfdene Goguen, Pierre Courtieu
+;; Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
+
+;; License:     GPL (GNU GENERAL PUBLIC LICENSE)
+
+;;; Commentary:
+;;
+
+;;; Code:
+
+(unless (locate-library "coq-mode")
+  (add-to-list 'load-path
+               (expand-file-name
+                (file-name-directory (or load-file-name buffer-file-name)))))
+
+;; (if t (require 'coq nil 'noerror))
+(require 'coq-smie)
+(require 'coq-syntax)                   ;For font-lock-keywords
+
+(defgroup coq-mode ()
+  "Major mode to edit Coq code."
+  :group 'programming)
+
+;; prettify is in emacs > 24.4
+;; FIXME: this should probably be done like for smie above.
+(defvar coq-may-use-prettify (fboundp 'prettify-symbols-mode))
+
+(defcustom coq-prog-name
+  (or (if (executable-find "coqtop") "coqtop")
+      (let ((exec-path (append exec-path '("C:/Program Files/Coq/bin"))))
+        (executable-find "coqtop"))
+      "coqtop")
+  "Name of program to run as Coq.
+On Windows with latest Coq package you might need something like:
+   C:/Program Files/Coq/bin/coqtop.opt.exe
+instead of just \"coqtop\".
+This must be a single program name with no arguments.  See option
+`coq-prog-args' to manually adjust the arguments to the Coq process.
+See also `coq-prog-env' to adjust the environment."
+  :type 'string
+  :group 'coq
+  :group 'coq-mode)
+
+(defun get-coq-library-directory ()
+  (let ((default-directory
+	  (if (file-accessible-directory-p default-directory)
+	      default-directory
+	    "/")))
+    (or (ignore-errors (car (process-lines coq-prog-name "-where")))
+	"/usr/local/lib/coq")))
+
+(defconst coq-library-directory (get-coq-library-directory) ;; FIXME Should be refreshed more often
+  "The coq library directory, as reported by \"coqtop -where\".")
+
+(defcustom coq-tags (expand-file-name "/theories/TAGS" coq-library-directory)
+  "The default TAGS table for the Coq library."
+  :type 'string)
+
+(defcustom coq-use-pg t
+  "If non-nil, activate the ProofGeneral backend."
+  :type 'boolean)
+
+;; prettify is in emacs > 24.4
+(defvar prettify-symbols-alist)
+
+(defconst coq-prettify-symbols-alist
+  '(("not"	. ?¬)
+    ;; ("/\\"	. ?∧)
+    ("/\\"	. ?⋀)
+    ;; ("\\/"	. ?∨)
+    ("\\/"	. ?⋁)
+    ;;("forall"	. ?∀)
+    ("forall"	. ?Π)
+    ("fun"	. ?λ)
+    ("->"	. ?→)
+    ("<-"	. ?←)
+    ("=>"	. ?⇒)
+    ;; ("~>"	. ?↝) ;; less desirable
+    ;; ("-<"	. ?↢) ;; Paterson's arrow syntax
+    ;; ("-<"	. ?⤙) ;; nicer but uncommon
+    ("::"	. ?∷)
+    ))
+
+(defvar coq-mode-map
+  (let ((map (make-sparse-keymap)))
+    map)
+  "Keymap for `coq-mode'.")
+
+(defvar coq-mode-syntax-table
+  (let ((st (make-syntax-table)))
+    (modify-syntax-entry ?\$ "." st)
+    (modify-syntax-entry ?\/ "." st)
+    (modify-syntax-entry ?\\ "." st)
+    (modify-syntax-entry ?+  "." st)
+    (modify-syntax-entry ?-  "." st)
+    (modify-syntax-entry ?=  "." st)
+    (modify-syntax-entry ?%  "." st)
+    (modify-syntax-entry ?<  "." st)
+    (modify-syntax-entry ?>  "." st)
+    (modify-syntax-entry ?\& "." st)
+    (modify-syntax-entry ?_  "_" st) ; beware: word consituent EXCEPT in head position
+    (modify-syntax-entry ?\' "_" st) ; always word constituent
+    (modify-syntax-entry ?∀ "." st)
+    (modify-syntax-entry ?∃ "." st)
+    (modify-syntax-entry ?λ "." st) ;; maybe a bad idea... lambda is a letter
+    (modify-syntax-entry ?\| "." st)
+
+    ;; Should maybe be "_" but it makes coq-find-and-forget (in coq.el) bug,
+    ;; hence the coq-with-altered-syntax-table to put "." into "_" class
+    ;; temporarily.
+    (modify-syntax-entry ?\. "." st)
+
+    (modify-syntax-entry ?\* ". 23n" st)
+    (modify-syntax-entry ?\( "()1" st)
+    (modify-syntax-entry ?\) ")(4" st)
+    st))
+
+;; FIXME, deal with interactive "Definition"
+(defvar coq-outline-regexp
+  ;;  (concat "(\\*\\|"
+  (concat "[ ]*" (regexp-opt
+                  '(
+                    "Ltac" "Corr" "Modu" "Sect" "Chap" "Goal"
+                    "Definition" "Lemm" "Theo" "Fact" "Rema"
+                    "Mutu" "Fixp" "Func")
+                  t)))
+
+(defvar coq-outline-heading-end-regexp "\\.[ \t\n]")
+
+(defun coq-near-comment-region ()
+  "Return a list of the forme (BEG END).
+BEG,END being is the comment region near position PT.
+Return nil if PT is not near a comment.
+Near here means PT is either inside or just aside of a comment."
+  (save-excursion
+    (let ((pos (point))
+          (ppss (syntax-ppss (1- (point)))))
+      (unless (nth 4 ppss)
+        ;; We're not squarely inside a comment, nor at its end.
+        ;; But we may still be at the beginning of a comment.
+        (setq ppss (syntax-ppss
+                    (+ pos (if (looking-at comment-start-skip) 2 1)))))
+      (when (nth 4 ppss)
+        (goto-char (nth 8 ppss))
+        (list (point)
+              (progn (forward-comment 1) (point)))))))
+
+
+(defun coq-fill-paragraph-function (_n)
+  "Coq mode specific fill-paragraph function. Fills only comment at point."
+  (let ((reg (coq-near-comment-region)))
+    (when reg
+      (fill-region (car reg) (cadr reg))))
+  t);; true to not fallback to standard fill function
+
+;; TODO (but only for paragraphs in comments)
+;; Should recognize coqdoc bullets, stars etc... Unplugged for now.
+(defun coq-adaptive-fill-function ()
+  (let ((reg (coq-near-comment-region)))
+    (save-excursion
+      (goto-char (car reg))
+      (re-search-forward "\\((\\*+ ?\\)\\( *\\)")
+      (let* ((cm-start (match-string 1))
+             (cm-prefix (match-string 2)))
+        (concat (make-string (length cm-start) ? ) cm-prefix)))))
+
+;;;###autoload
+(add-to-list 'auto-mode-alist '("\\.v\\'" . coq-mode))
+
+(defun coq--parent-mode ()
+  (if coq-use-pg (proof-mode) (prog-mode)))
+
+;;;###autoload
+(define-derived-mode coq-mode coq--parent-mode "Coq"
+  "Major mode for Coq scripts.
+
+\\{coq-mode-map}"
+  ;; SMIE needs this.
+  (set (make-local-variable 'parse-sexp-ignore-comments) t)
+  ;; Coq error messages are thrown off by TAB chars.
+  (set (make-local-variable 'indent-tabs-mode) nil)
+  ;; Coq defninition never start by a parenthesis
+  (set (make-local-variable 'open-paren-in-column-0-is-defun-start) nil)
+  ;; do not break lines in code when filling
+  (set (make-local-variable 'fill-nobreak-predicate)
+       (lambda () (not (nth 4 (syntax-ppss)))))
+  ;; coq mode specific indentation function
+  (set (make-local-variable 'fill-paragraph-function)
+       #'coq-fill-paragraph-function)
+
+  ;; TODO (but only for paragraphs in comments)
+  ;; (set (make-local-variable 'paragraph-start)  "[ 	]*\\((\\**\\|$\\)")
+  ;; (set (make-local-variable 'paragraph-separate) "\\**) *$\\|$")
+  ;; (set (make-local-variable 'adaptive-fill-function)
+  ;;      #'coq-adaptive-fill-function)
+
+  (set (make-local-variable 'comment-start-skip)  "(\\*+ *")
+  (set (make-local-variable 'comment-end-skip) " *\\*+)")
+
+  (smie-setup coq-smie-grammar #'coq-smie-rules
+              :forward-token #'coq-smie-forward-token
+              :backward-token #'coq-smie-backward-token)
+
+  ;; old indentation code.
+  ;; (require 'coq-indent)
+  ;; (setq
+  ;;  ;; indentation is implemented in coq-indent.el
+  ;;  indent-line-function #'coq-indent-line
+  ;;  proof-indent-any-regexp      coq-indent-any-regexp
+  ;;  proof-indent-open-regexp     coq-indent-open-regexp
+  ;;  proof-indent-close-regexp    coq-indent-close-regexp)
+  ;; (set (make-local-variable 'indent-region-function) #'coq-indent-region)
+
+  ;; we can cope with nested comments
+  (set (make-local-variable 'comment-quote-nested) nil)
+
+  ;; FIXME: have abbreviation without holes
+  ;(if coq-use-editing-holes (holes-mode 1))
+  (if (fboundp 'holes-mode) (holes-mode 1))
+
+  ;; Setup Proof-General interface to Coq.
+  (if coq-use-pg (coq-pg-setup))
+
+  ;; font-lock
+  (setq-local font-lock-defaults '(coq-font-lock-keywords-1))
+
+  ;; outline
+  (setq-local outline-regexp coq-outline-regexp)
+  (setq-local outline-heading-end-regexp coq-outline-heading-end-regexp)
+
+  ;; tags
+  (if (file-exists-p coq-tags)
+      (set (make-local-variable 'tags-table-list)
+           (cons coq-tags tags-table-list)))
+
+  (set (make-local-variable 'blink-matching-paren-dont-ignore-comments) t)
+
+  (when coq-may-use-prettify
+    (set (make-local-variable 'prettify-symbols-alist)
+         coq-prettify-symbols-alist)))
+
+(provide 'coq-mode)
+
+;; Local Variables: ***
+;; fill-column: 79 ***
+;; indent-tabs-mode: nil ***
+;; coding: utf-8 ***
+;; End: ***
+
+;;; coq-mode.el ends here
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 7a11a43f..30f1a374 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -1454,34 +1454,6 @@ part of another hypothesis.")
 
 
 
-(defun coq-init-syntax-table ()
-  "Set appropriate values for syntax table in current buffer."
-
-  (modify-syntax-entry ?\$ ".")
-  (modify-syntax-entry ?\/ ".")
-  (modify-syntax-entry ?\\ ".")
-  (modify-syntax-entry ?+  ".")
-  (modify-syntax-entry ?-  ".")
-  (modify-syntax-entry ?=  ".")
-  (modify-syntax-entry ?%  ".")
-  (modify-syntax-entry ?<  ".")
-  (modify-syntax-entry ?>  ".")
-  (modify-syntax-entry ?\& ".")
-  (modify-syntax-entry ?_  "_") ; beware: word consituent EXCEPT in head position
-  (modify-syntax-entry ?\' "_") ; always word constituent
-  (modify-syntax-entry ?∀ ".")
-  (modify-syntax-entry ?∃ ".")
-  (modify-syntax-entry ?λ ".") ;; maybe a bad idea... lambda is a letter
-  (modify-syntax-entry ?\| ".")
-
-  ;; should maybe be "_" but it makes coq-find-and-forget (in coq.el) bug
-  ;; Hence the coq-with-altered-syntax-table below to put "." into "_" class temporarily
-  (modify-syntax-entry ?\. ".")
-
-  (modify-syntax-entry ?\* ". 23n")
-  (modify-syntax-entry ?\( "()1")
-  (modify-syntax-entry ?\) ")(4"))
-
 ;; use this to evaluate code with "." being consisdered a symbol
 ;; constituent (better behavior for thing-at and maybe font-lock too,
 ;; for indentation we use ad hoc smie lexers).
diff --git a/coq/coq-system.el b/coq/coq-system.el
index e89a0fdb..44a774ae 100644
--- a/coq/coq-system.el
+++ b/coq/coq-system.el
@@ -24,6 +24,7 @@
 ;;; Code:
 
 (require 'proof)
+(require 'coq-mode)                     ;for coq-prog-name
 
 (defvar coq-prog-args)
 (defvar coq-debug)
@@ -43,19 +44,6 @@ On Windows you might need something like:
   (setq coq-prog-env '(\"HOME=C:\\Program Files\\Coq\\\"))"
   :group 'coq)
 
-(defcustom coq-prog-name
-  (if (executable-find "coqtop") "coqtop"
-    (proof-locate-executable "coqtop" t '("C:/Program Files/Coq/bin")))
-  "*Name of program to run as Coq.  See `proof-prog-name', set from this.
-On Windows with latest Coq package you might need something like:
-   C:/Program Files/Coq/bin/coqtop.opt.exe
-instead of just \"coqtop\".
-This must be a single program name with no arguments.  See option
-`coq-prog-args' to manually adjust the arguments to the Coq process.
-See also `coq-prog-env' to adjust the environment."
-  :type 'string
-  :group 'coq)
-
 (defcustom coq-dependency-analyzer
   (if (executable-find "coqdep") "coqdep"
     (proof-locate-executable "coqdep" t '("C:/Program Files/Coq/bin")))
@@ -70,22 +58,6 @@ See also `coq-prog-env' to adjust the environment."
   :type 'string
   :group 'coq)
 
-(defun get-coq-library-directory ()
-  (let ((default-directory
-	  (if (file-accessible-directory-p default-directory)
-	      default-directory
-	    "/")))
-    (or (ignore-errors (car (process-lines coq-prog-name "-where")))
-	"/usr/local/lib/coq")))
-
-(defconst coq-library-directory (get-coq-library-directory) ;; FIXME Should be refreshed more often
-  "The coq library directory, as reported by \"coqtop -where\".")
-
-(defcustom coq-tags (concat coq-library-directory "/theories/TAGS")
-  "The default TAGS table for the Coq library."
-  :type 'string
-  :group 'coq)
-
 (defcustom coq-pinned-version nil
   "Which version of Coq you are using.
 There should be no need to set this value unless you use the trunk from
diff --git a/coq/coq.el b/coq/coq.el
index 06a01855..29a6c1ad 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -19,6 +19,16 @@
 
 ;;; Code:
 
+;; PG doesn't support using several backends at the same time.
+;; FIXME: We really should set proof-assistant just because this file is
+;; loaded (e.g. we should set it within coq-pg-setup instead), but
+;; defpacustom and various others fail if executed before proof-assistant
+;; is set.
+(if (and (boundp 'proof-assistant)
+         (member proof-assistant '(nil "" "Coq" "coq")))
+    (proof-ready-for-assistant 'coq)
+  (message "Coq-PG error: Proof General already in use for %s" proof-assistant))
+
 (require 'cl-lib)
 
 (require 'span)
@@ -43,15 +53,11 @@
 (require 'proof)
 (require 'coq-system)                   ; load path, option, project file etc.
 (require 'coq-syntax)                   ; font-lock, syntax categories (tactics, commands etc)
-(require 'coq-local-vars)               ; setting coq args via file variables 
+(require 'coq-local-vars)               ; setting coq args via file variables
                                         ;   (prefer _CoqProject file instead)
 (require 'coq-abbrev)                   ; abbrev and coq specific menu
 (require 'coq-seq-compile)              ; sequential compilation of Requires
 (require 'coq-par-compile)              ; parallel compilation of Requires
-
-;; prettify is in emacs > 24.4
-;; FIXME: this should probably be done like for smie above.
-(defvar coq-may-use-prettify (fboundp 'prettify-symbols-mode))
 (defvar prettify-symbols-alist)
 
 
@@ -81,7 +87,7 @@ These are appended at the end of `coq-shell-init-cmd'."
   :group 'coq)
 
 ;; Default coq is only Private_ and _subproof
-(defcustom coq-search-blacklist-string ; add this? \"_ind\" \"_rect\" \"_rec\" 
+(defcustom coq-search-blacklist-string ; add this? \"_ind\" \"_rect\" \"_rec\"
  "\"Private_\" \"_subproof\""
   "String for blacklisting strings from requests to Coq environment."
   :type 'string
@@ -161,7 +167,7 @@ See also option `coq-hide-additional-subgoals'."
 
 ;; Ignore all commands that start a proof. Otherwise "Proof" will appear
 ;; as superfluous node in the proof tree. Note that we cannot ignore Proof,
-;; because, Fixpoint does not display the proof goal, see Coq bug #2776. 
+;; because, Fixpoint does not display the proof goal, see Coq bug #2776.
 (defcustom coq-proof-tree-ignored-commands-regexp
   (concat "^\\(\\(Show\\)\\|\\(Locate\\)\\|"
           "\\(Theorem\\)\\|\\(Lemma\\)\\|\\(Remark\\)\\|\\(Fact\\)\\|"
@@ -264,18 +270,6 @@ See also option `coq-hide-additional-subgoals'."
 ;; Outline mode
 ;;
 
-;; FIXME, deal with interacive "Definition"
-(defvar coq-outline-regexp
-;;  (concat "(\\*\\|"
-  (concat "[ ]*" (regexp-opt
-                  '(
-                    "Ltac" "Corr" "Modu" "Sect" "Chap" "Goal"
-                    "Definition" "Lemm" "Theo" "Fact" "Rema"
-                    "Mutu" "Fixp" "Func") t)))
-;;)
-
-(defvar coq-outline-heading-end-regexp "\\.[ \t\n]")
-
 (defvar coq-shell-outline-regexp coq-goal-regexp)
 (defvar coq-shell-outline-heading-end-regexp coq-goal-regexp)
 
@@ -298,6 +292,10 @@ See also option `coq-hide-additional-subgoals'."
 ;; Derived modes
 ;;
 
+(defvar coq-shell-mode-syntax-table coq-mode-syntax-table)
+(defvar coq-response-mode-syntax-table coq-mode-syntax-table)
+(defvar coq-goals-mode-syntax-table coq-mode-syntax-table)
+
 (define-derived-mode coq-shell-mode proof-shell-mode
   "Coq Shell" nil
   (coq-shell-mode-config))
@@ -305,21 +303,10 @@ See also option `coq-hide-additional-subgoals'."
 (define-derived-mode coq-response-mode proof-response-mode
   "Coq Response" nil
   (coq-response-config))
-
-(define-derived-mode coq-mode proof-mode "Coq"
-  "Major mode for Coq scripts.
-
-\\{coq-mode-map}"
-  (coq-mode-config))
-
 (define-derived-mode coq-goals-mode proof-goals-mode
   "Coq Goals" nil
   (coq-goals-mode-config))
 
-;; Indentation and navigation support via SMIE.
-
-(require 'coq-smie)
-
 ;;
 ;; Auxiliary code for Coq modes
 ;;
@@ -385,7 +372,7 @@ annotation-start) if found."
 ;; This is a modified version of the same function in generic/proof-shell.el.
 ;; Using function coq-search-urgent-message instead of regex
 ;; proof-shell-eager-annotation-start, in order to let non urgent message as
-;; such. i.e. "Time" messages. 
+;; such. i.e. "Time" messages.
 (defun proof-shell-process-urgent-messages ()
   "Scan the shell buffer for urgent messages.
 Scanning starts from `proof-shell-urgent-message-scanner' or
@@ -424,7 +411,7 @@ This is a subroutine of `proof-shell-filter'."
     ;; Set position of last urgent message found
     (if lastend
 	(set-marker proof-shell-urgent-message-marker lastend))
-	
+
     (goto-char pt)))
 
 ;; Due to the architecture of proofgeneral, informative message put *before*
@@ -456,13 +443,13 @@ This is a subroutine of `proof-shell-filter'."
     (pg-response-display-with-face strnotrailingspace))) ; face
 
 
-;;;;;;;;;;; Trying to accept { and } as terminator for empty commands. Actually
-;;;;;;;;;;; I am experimenting two new commands "{" and "}" (without no
-;;;;;;;;;;; trailing ".") which behave like BeginSubProof and EndSubproof. The
-;;;;;;;;;;; absence of a trailing "." makes it difficult to distinguish between
-;;;;;;;;;;; "{" of normal coq code (implicits, records) and this the new
-;;;;;;;;;;; commands. We therefore define a coq-script-parse-function to this
-;;;;;;;;;;; purpose.
+;; Trying to accept { and } as terminator for empty commands. Actually
+;; I am experimenting two new commands "{" and "}" (without no
+;; trailing ".") which behave like BeginSubProof and EndSubproof. The
+;; absence of a trailing "." makes it difficult to distinguish between
+;; "{" of normal coq code (implicits, records) and this the new
+;; commands. We therefore define a coq-script-parse-function to this
+;; purpose.
 
 ;; coq-end-command-regexp is ni coq-indent.el
 (defconst coq-script-command-end-regexp coq-end-command-regexp)
@@ -981,7 +968,7 @@ UNSETCMD.  See `coq-command-with-set-unset'."
 
 
   ;; (let* ((cmd) (postform (if (eq postformatcmd nil) 'identity postformatcmd)))
-    
+
 
   ;;   (proof-shell-ready-prover)
   ;;   (setq cmd (coq-guess-or-ask-for-string ask dontguess))
@@ -1218,7 +1205,7 @@ be called and no command will be sent to Coq."
      ;; If closing a nested proof, Show the enclosing goal.
      (and (string-match coq-save-command-regexp-strict cmd)
           (> (length coq-last-but-one-proofstack) 1))
-     ;; If user issued a printing option then t printing. 
+     ;; If user issued a printing option then t printing.
      (and (string-match "\\(S\\|Uns\\)et\\s-+Printing" cmd)
           (> (length coq-last-but-one-proofstack) 0)))
     (list "Show."))
@@ -1285,7 +1272,7 @@ necessary.")
   (coq-buffer-window-width proof-goals-buffer))
 (defun coq-response-window-width ()
   (coq-buffer-window-width proof-response-buffer))
- 
+
 (defun coq-guess-goal-buffer-at-next-command ()
   "Return the probable width of goals buffer if it pops up now.
 This is a guess based on the current width of goals buffer if
@@ -1400,7 +1387,7 @@ Maintained by a hook in `proof-shell-handle-delayed-output-hook'.")
 ;; coq-hyp...faces
 (defun coq-make-hypcross-overlay (beg end h buf)
   (let ((ov (make-overlay beg end buf)))
-    (when ov 
+    (when ov
       (overlay-put ov 'evaporate t)
       (overlay-put ov 'is-hypcross t)
       (overlay-put ov 'hyp-name h)
@@ -1441,7 +1428,7 @@ Maintained by a hook in `proof-shell-handle-delayed-output-hook'.")
       (mapc
        (lambda (s)
          (setq res
-               (cons 
+               (cons
                 (cons (substring-no-properties s)
                       (cons hypov (cons hypnameov (cons crosshypov nil)) ))
                 res)))
@@ -1601,7 +1588,7 @@ See  `coq-highlight-hyp'."
           (or (car (coq-overlays-at pt 'hyp-name))
               ;; we may be between hypname and hyp, so skip backward to
               ;; something meaningful
-              (save-excursion                
+              (save-excursion
                 (goto-char pt)
                 (search-backward-regexp "[^ :=]\\|\n")
                 (car (coq-overlays-at (point) 'hyp-name)))))
@@ -1663,7 +1650,7 @@ Used on hyptohesis overlays in goals buffer mainly."
            (prefx (make-string (min 8 lgthhyp) ?.))
            (hypcross-ov (overlay-get hyp-overlay 'hypcross-ov)))
       (overlay-put
-       hyp-overlay 'display 
+       hyp-overlay 'display
        prefx ;(propertize prefx 'keymap coq-hidden-hyp-map)
        )
       (overlay-put hyp-overlay 'evaporate t)
@@ -1814,70 +1801,6 @@ See  `coq-fold-hyp'."
 ;; *default* value to nil.
 (custom-set-default 'proof-output-tooltips nil)
 
-(defconst coq-prettify-symbols-alist
-  '(("not"	. ?¬)
-    ;; ("/\\"	. ?∧)
-    ("/\\"	. ?⋀)
-    ;; ("\\/"	. ?∨)
-    ("\\/"	. ?⋁)
-    ;;("forall"	. ?∀)
-    ("forall"	. ?Π)
-    ("fun"	. ?λ)
-    ("->"	. ?→)
-    ("<-"	. ?←)
-    ("=>"	. ?⇒)
-    ;; ("~>"	. ?↝) ;; less desirable
-    ;; ("-<"	. ?↢) ;; Paterson's arrow syntax
-    ;; ("-<"	. ?⤙) ;; nicer but uncommon
-    ("::"	. ?∷)
-    ))
-
-
-(defun coq-get-comment-region (pt)
-  "Return a list of the form (BEG END).
-BEG,END being the comment region arount position PT.
-Return nil if PT is not inside a comment."
-  (save-excursion
-    (goto-char pt)
-    `(,(save-excursion (coq-find-comment-start))
-      ,(save-excursion (coq-find-comment-end)))))
-
-(defun coq-near-comment-region ()
-  "Return a list of the forme (BEG END).
-BEG,END being is the comment region near position PT.
-Return nil if PT is not near a comment.
-Near here means PT is either inside or just aside of a comment."
-  (save-excursion
-    (cond
-     ((coq-looking-at-comment)
-      (coq-get-comment-region (point)))
-     ((and (looking-back proof-script-comment-end nil)
-           (save-excursion (forward-char -1) (coq-looking-at-comment)))
-      (coq-get-comment-region (- (point) 1)))
-     ((and (looking-at proof-script-comment-start)
-           (save-excursion (forward-char) (coq-looking-at-comment)))
-      (coq-get-comment-region (+ (point) 1))))))
-
-(defun coq-fill-paragraph-function (n)
-  "Coq mode specific fill-paragraph function. Fills only comment at point."
-  (let ((reg (coq-near-comment-region)))
-    (when reg
-      (fill-region (car reg) (cadr reg))))
-  t);; true to not fallback to standard fill function
-
-;; TODO (but only for paragraphs in comments)
-;; Should recognize coqdoc bullets, stars etc... Unplugged for now.
-(defun coq-adaptive-fill-function ()
-  (let ((reg (coq-near-comment-region)))
-    (save-excursion
-      (goto-char (car reg))
-      (re-search-forward "\\((\\*+ ?\\)\\( *\\)")
-      (let* ((cm-start (match-string 1))
-             (cm-prefix (match-string 2)))
-        (concat (make-string (length cm-start) ? ) cm-prefix)))))
-
-
-
 ;;;;;;;;;;;;;;;;;;;;;;;attempt to deal with debug mode ;;;;;;;;;;;;;;;;
 
 ;; tries to extract the last debug goal and display it in goals buffer
@@ -1908,25 +1831,26 @@ Near here means PT is either inside or just aside of a comment."
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-
-(defun coq-mode-config ()
-  ;; SMIE needs this.
-  (set (make-local-variable 'parse-sexp-ignore-comments) t)
-  ;; Coq error messages are thrown off by TAB chars.
-  (set (make-local-variable 'indent-tabs-mode) nil)
-  ;; Coq defninition never start by a parenthesis
-  (set (make-local-variable 'open-paren-in-column-0-is-defun-start) nil)
-  ;; do not break lines in code when filling
-  (set (make-local-variable 'fill-nobreak-predicate)
-       (lambda () (not (nth 4 (syntax-ppss)))))
-  ;; coq mode specific indentation function
-  (set (make-local-variable 'fill-paragraph-function) 'coq-fill-paragraph-function)
-
-  ;; TODO (but only for paragraphs in comments)
-  ;; (set (make-local-variable 'paragraph-start)  "[ 	]*\\((\\**\\|$\\)")
-  ;; (set (make-local-variable 'paragraph-separate) "\\**) *$\\|$")
-  ;; (set (make-local-variable 'adaptive-fill-function) 'coq-adaptive-fill-function)
-
+(defvar coq-pg-mode-map
+  (let ((map (make-sparse-keymap)))
+    (set-keymap-parent map proof-mode-map)
+
+    ;;(define-key coq-mode-map coq-double-hit-hot-key 'coq-terminator-insert)
+
+    ;; Setting the new mapping for terminator, overrides the following in
+    ;; proof-script:
+    ;; (define-key proof-mode-map (vector (aref proof-terminal-string 0))
+    ;;             #'proof-electric-terminator)
+    ;;(define-key proof-mode-map (kbd coq-double-hit-hot-key)
+    ;;            #'coq-terminator-insert)
+    (define-key map (kbd ".") #'coq-terminator-insert)
+    ;;(define-key map (kbd ";") #'coq-terminator-insert) ; for french keyboards
+    map))
+
+;;;###autoload
+(defun coq-pg-setup ()
+  (set-keymap-parent (current-local-map) coq-pg-mode-map)
+  
   ;; coq-mode colorize errors better than the generic mechanism
   (setq proof-script-color-error-messages nil)
   (setq proof-terminal-string ".")
@@ -1935,8 +1859,6 @@ Near here means PT is either inside or just aside of a comment."
   (setq proof-script-comment-start "(*")
   (setq proof-script-comment-end "*)")
   (setq proof-script-insert-newlines nil)
-  (set (make-local-variable 'comment-start-skip)  "(\\*+ *")
-  (set (make-local-variable 'comment-end-skip) " *\\*+)")
   (setq proof-unnamed-theorem-name "Unnamed_thm") ; Coq's default name
 
   (setq proof-assistant-home-page coq-www-home-page)
@@ -1948,7 +1870,7 @@ Near here means PT is either inside or just aside of a comment."
   ;; We manage file saveing via coq-compile-auto-save and for coq
   ;; it is not necessary to save files when starting a new buffer.
   (setq proof-query-file-save-when-activating-scripting nil)
-  
+
   ;; Commands sent to proof engine
   (setq proof-showproof-command "Show. "
         proof-context-command "Print All. "
@@ -1983,40 +1905,12 @@ Near here means PT is either inside or just aside of a comment."
 	proof-nested-undo-regexp coq-state-changing-commands-regexp
         proof-script-imenu-generic-expression coq-generic-expression)
 
-  (smie-setup coq-smie-grammar #'coq-smie-rules
-              :forward-token #'coq-smie-forward-token
-              :backward-token #'coq-smie-backward-token)
-
-  ;; old indentation code.
-  ;; (require 'coq-indent)
-  ;; (setq
-  ;;  ;; indentation is implemented in coq-indent.el
-  ;;  indent-line-function 'coq-indent-line
-  ;;  proof-indent-any-regexp      coq-indent-any-regexp
-  ;;  proof-indent-open-regexp     coq-indent-open-regexp
-  ;;  proof-indent-close-regexp    coq-indent-close-regexp)
-  ;; (make-local-variable 'indent-region-function)
-  ;; (setq indent-region-function 'coq-indent-region)
-  
-  
-
   ;; span menu
-  (setq proof-script-span-context-menu-extensions 'coq-create-span-menu)
+  (setq proof-script-span-context-menu-extensions #'coq-create-span-menu)
 
   (setq proof-shell-start-silent-cmd "Set Silent. "
         proof-shell-stop-silent-cmd "Unset Silent. ")
 
-  (coq-init-syntax-table)
-  ;; we can cope with nested comments
-  (set (make-local-variable 'comment-quote-nested) nil)
-
-  ;; font-lock
-  (setq proof-script-font-lock-keywords coq-font-lock-keywords-1)
-
-  ;; FIXME: have abbreviation without holes
-  ;(if coq-use-editing-holes (holes-mode 1))
-  (holes-mode 1)
-
   ;; prooftree config
   (setq
    proof-tree-configured t
@@ -2024,27 +1918,10 @@ Near here means PT is either inside or just aside of a comment."
    proof-tree-find-begin-of-unfinished-proof
      'coq-find-begin-of-unfinished-proof)
 
-  (proof-config-done)
-
-  ;; outline
-  (set (make-local-variable 'outline-regexp) coq-outline-regexp)
-  (set (make-local-variable 'outline-heading-end-regexp)
-       coq-outline-heading-end-regexp)
-
-  ;; tags
-  (if (file-exists-p coq-tags)
-      (set (make-local-variable 'tags-table-list)
-           (cons coq-tags tags-table-list)))
-  
-  (set (make-local-variable 'blink-matching-paren-dont-ignore-comments) t)
-
-  (when coq-may-use-prettify
-    (set (make-local-variable 'prettify-symbols-alist)
-         coq-prettify-symbols-alist))
-
   (setq proof-cannot-reopen-processed-files nil)
 
-  (add-hook 'proof-activate-scripting-hook #'proof-cd-sync nil t))
+  (proof-config-done)
+  )
 
 (defun coq-shell-mode-config ()
   (setq
@@ -2095,7 +1972,6 @@ Near here means PT is either inside or just aside of a comment."
    proof-shell-restart-cmd coq-shell-restart-cmd
    pg-subterm-anns-use-stack t)
 
-  (coq-init-syntax-table)
   ;; (holes-mode 1)  da: does the shell really need holes mode on?
   (setq proof-shell-font-lock-keywords 'coq-font-lock-keywords-1)
 
@@ -2120,7 +1996,7 @@ Near here means PT is either inside or just aside of a comment."
    proof-tree-show-sequent-command 'coq-show-sequent-command
    proof-tree-find-undo-position 'coq-proof-tree-find-undo-position
    )
-        
+
   (proof-shell-config-done))
 
 
@@ -2140,12 +2016,10 @@ Near here means PT is either inside or just aside of a comment."
 (defun coq-goals-mode-config ()
   (setq pg-goals-change-goal "Show %s . ")
   (setq pg-goals-error-regexp coq-error-regexp)
-  (coq-init-syntax-table)
   (setq proof-goals-font-lock-keywords coq-goals-font-lock-keywords)
   (proof-goals-config-done))
 
 (defun coq-response-config ()
-  (coq-init-syntax-table)
   (setq proof-response-font-lock-keywords coq-response-font-lock-keywords)
   ;; The line wrapping in this buffer just seems to make it less readable.
   (setq truncate-lines t)
@@ -2192,7 +2066,7 @@ Near here means PT is either inside or just aside of a comment."
   :type 'integer
   :setting "Set Printing Depth %i . ")
 
-;;; Obsolete:
+;; Obsolete:
 ;;(defpacustom undo-depth coq-default-undo-limit
 ;;  "Depth of undo history.  Undo behaviour will break beyond this size."
 ;;  :type 'integer
@@ -2309,7 +2183,7 @@ The not yet delayed output is in the region
                              no-response-display
                              proof-tree-show-subgoal))
                           proof-action-list))))))))))
-  
+
 (add-hook 'proof-tree-urgent-action-hook #'coq-proof-tree-get-new-subgoals)
 
 
@@ -2330,7 +2204,7 @@ The not yet delayed output is in the region
              (span-property span 'goalcmd))
         (span-start span)
       nil)))
-    
+
 (defun coq-proof-tree-find-undo-position (state)
   "Return the position for undo state STATE.
 This is the Coq incarnation of `proof-tree-find-undo-position'."
@@ -2621,7 +2495,7 @@ Based on idea mentioned in Coq reference manual."
 (defvar coq-keywords-accepting-as-regex (regexp-opt '("induction" "destruct" "inversion" "injection")))
 
 ;; destruct foo., where foo is a name.
-(defvar coq-auto-as-hack-hyp-name-regex 
+(defvar coq-auto-as-hack-hyp-name-regex
   (concat "\\(" "induction\\|destruct" "\\)\\s-+\\(" coq-id-shy "\\)\\s-*\\.")
   "Regexp of commands needing a hack to generate correct \"as\" close.
 tacitcs like destruct and induction reuse hypothesis names by
@@ -2635,7 +2509,7 @@ Warning: this makes the error messages (and location) wrong.")
 (defun coq-hack-cmd-for-infoH (s)
   "return the tactic S hacked with infoH tactical."
   (cond
-   ((string-match ";" s) s) ;; composed tactic cannot be treated 
+   ((string-match ";" s) s) ;; composed tactic cannot be treated
    ((string-match coq-auto-as-hack-hyp-name-regex s)
     (concat "infoH " (match-string 1 s) " (" (match-string 2 s) ")."))
    ((string-match coq-keywords-accepting-as-regex s)
@@ -2792,7 +2666,7 @@ Completion is on a quasi-exhaustive list of Coq tacticals."
 (define-key coq-keymap [(control ?q)] 'coq-query)
 (define-key coq-keymap [(control ?r)] 'coq-insert-requires)
 ; [ for "as [xxx]" is easy to remember, ccontrol-[ would be better but hard to type on french keyboards
-; anyway company-coq should provide an "as!<TAB>". 
+; anyway company-coq should provide an "as!<TAB>".
 (define-key coq-keymap [(?\[)] 'coq-insert-as-in-next-command) ;; not for goal/response buffer?
 
 ; Query commands
@@ -2882,13 +2756,13 @@ Completion is on a quasi-exhaustive list of Coq tacticals."
 
 ;; Default binding: clicking on the cross to folds/unfold hyp.
 ;; Click on it with button 2 copies the names at current point.
-(when coq-hypname-map 
+(when coq-hypname-map
   (define-key coq-hypcross-map [(mouse-1)] 'coq-toggle-fold-hyp-at-mouse)
   (define-key coq-hypcross-map [return] 'coq-toggle-fold-hyp-at-point)
   (define-key coq-hypcross-map [(mouse-2)] 'coq-insert-at-point-hyp-at-mouse))
 ;; Ddefault binding: clicking on a hidden hyp with button 3 unfolds it, with
 ;; button 2 it copies hyp name at current point.
-(when coq-hidden-hyp-map 
+(when coq-hidden-hyp-map
   (define-key coq-hidden-hyp-map [(mouse-3)] 'coq-toggle-fold-hyp-at-mouse)
   (define-key coq-hidden-hyp-map [(mouse-2)] 'coq-insert-at-point-hyp-at-mouse))
 
@@ -2979,7 +2853,7 @@ buffer."
               (lgth (cadr mtch)))
           (goto-char (+ (proof-unprocessed-begin) 1))
           (coq-find-real-start)
-          
+
           ;; utf8 adaptation is made in coq-get-last-error-location above
           (let ((time-offset (if coq-time-commands (length coq--time-prefix) 0)))
             (goto-char (+ (point) pos))
@@ -3126,7 +3000,7 @@ Only when three-buffer-mode is enabled."
   ;; https://github.com/cpitclaudel/company-coq/issues/8.
   (unless (memq 'no-response-display proof-shell-delayed-output-flags)
     ;; If there is no frame with goql+response then do nothing
-    (when proof-three-window-enable 
+    (when proof-three-window-enable
       (let ((threeb-frames (coq-find-threeb-frames)))
         (when threeb-frames
           (let ((pg-frame (car threeb-frames))) ; selecting one adequate frame
@@ -3149,7 +3023,7 @@ Only when three-buffer-mode is enabled."
                         (goto-char (point-min))
                         (recenter)))))))))))))
 
-;; TODO: remove/add hook instead? 
+;; TODO: remove/add hook instead?
 (defun coq-optimise-resp-windows-if-option ()
   (when coq-optimise-resp-windows-enable (coq-optimise-resp-windows)))
 
@@ -3200,7 +3074,7 @@ It will be restored if double hit terminator is toggle off.")
 
 ;; We redefine the keybinding when we go in and out of double hit mode, even if
 ;; in principle coq-terminator-insert is compatible with
-;; proof-electric-terminator. This may be overprudent but I suspect that  
+;; proof-electric-terminator. This may be overprudent but I suspect that
 (defun coq-double-hit-enable ()
   "Disables electric terminator since double hit is a replacement.
 This function is called by `proof-set-value' on `coq-double-hit-enable'."
@@ -3216,8 +3090,6 @@ This function is called by `proof-set-value' on `coq-double-hit-enable'."
 
 
 
-;;(define-key coq-mode-map coq-double-hit-hot-key 'coq-terminator-insert)
-
 (proof-deftoggle coq-double-hit-enable coq-double-hit-toggle)
 
 (defadvice proof-electric-terminator-enable (after coq-unset-double-hit-advice)
@@ -3279,18 +3151,11 @@ priority to the former."
 
 (put 'coq-terminator-insert 'delete-selection t)
 
-;; Setting the new mapping for terminator, overrides the following in proof-script:
-;; (define-key proof-mode-map (vector (aref proof-terminal-string 0)) 'proof-electric-terminator)
-
-;(define-key proof-mode-map (kbd coq-double-hit-hot-key) 'coq-terminator-insert)
-(define-key coq-mode-map (kbd ".") 'coq-terminator-insert)
-;(define-key coq-mode-map (kbd ";") 'coq-terminator-insert) ; for french keyboards
-
 ;;;;;;;;;;;;;;
 
 ;; This was done in coq-compile-common, but it is actually a good idea even
 ;; when "compile when require" is off. When switching scripting buffer, let us
-;; restart the coq shell process, so that it applies local coqtop options. 
+;; restart the coq shell process, so that it applies local coqtop options.
 (add-hook 'proof-deactivate-scripting-hook
           #'coq-switch-buffer-kill-proof-shell ;; this function is in coq-compile-common
           t)
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
diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el
index 095b108c..4b5f2e4a 100644
--- a/isar/isar-syntax.el
+++ b/isar/isar-syntax.el
@@ -1,4 +1,4 @@
-;; isar-syntax.el Syntax expressions for Isabelle/Isar
+;; isar-syntax.el Syntax expressions for Isabelle/Isar  -*- lexical-binding:t -*-
 ;; Copyright (C) 1994-2004, 2009, 2010 LFCS Edinburgh.
 ;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
 ;;
@@ -364,18 +364,18 @@ matches contents of quotes for quoted identifiers.")
 ;; font-lock syntactic fontification
 
 ;; adapted from font-lock.el in GNU Emacs 23.1.1
-(defun isar-font-lock-fontify-syntactically-region 
-  (start end &optional loudly ppss)
-  "Put proper face on each string and comment between START and END.
-START should be at the beginning of a line."
-  (let ((comment-end-regexp
-	 (replace-regexp-in-string "^ *" "" comment-end))
-        state beg)
-    (if loudly (message "Fontifying %s... (syntactically...)" (buffer-name)))
-    (goto-char start)
-    ;;
-    ;; Find the `start' state.
-    (setq state (or ppss (syntax-ppss start)))
+;; FIXME: Why not use the built-in syntactic fontification?
+(defun isar-font-lock-fontify-syntactically-region
+  (end) ;; (start end &optional loudly ppss)
+  "Put proper face on each string and comment between point and END."
+  (let (;; (comment-end-regexp
+	;;  (replace-regexp-in-string "^ *" "" comment-end))
+        (start (point))
+        ;; Find the start state.
+        (state (syntax-ppss))
+        beg)
+    (if font-lock-verbose ;; loudly
+        (message "Fontifying %s... (syntactically...)" (buffer-name)))
     ;;
     ;; Find each interesting place between here and `end'.
     (while
@@ -395,13 +395,16 @@ START should be at the beginning of a line."
 	      (put-text-property beg (point) 'face font-lock-comment-face))))
 	  (< (point) end))
       (setq state (parse-partial-sexp (point) end nil nil state
-				      'syntax-table)))))
+				      'syntax-table))))
+  ;; Job is done, return to font-lock-keywords that there's no match.
+  nil)
 
 ;; font-lock keywords fontification
 
 (defvar isar-font-lock-keywords-1
   (list
-   (cons 'isar-match-nesting                               'font-lock-preprocessor-face)
+   (list #'isar-font-lock-fontify-syntactically-region)
+   (cons #'isar-match-nesting                               'font-lock-preprocessor-face)
    (cons (isar-ids-to-regexp isar-keywords-minor)          'font-lock-type-face)
    (cons (isar-ids-to-regexp isar-keywords-control)        'proof-error-face)
    (cons (isar-ids-to-regexp isar-keywords-diag)           'proof-tacticals-name-face)
diff --git a/lib/bufhist.el b/lib/bufhist.el
index 65d33cc5..7e96682c 100644
--- a/lib/bufhist.el
+++ b/lib/bufhist.el
@@ -3,7 +3,7 @@
 ;; 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 2003-2018  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
@@ -179,8 +179,7 @@ This is as a pair (POINT . CONTENTS)."
   (if (and
        bufhist-mode
        (memq 'bufhist-before-change-function before-change-functions))
-      (let ((before-change-functions nil)
-	    (after-change-functions nil))
+      (let ((inhibit-modification-hooks t))
 	(bufhist-before-change-function)))
   (erase-buffer)
   (bufhist-insert-buttons))