From f7cc8f1f76baf5e517e51f1db47510ed605064e8 Mon Sep 17 00:00:00 2001 From: Stefan Monnier Date: Tue, 18 Dec 2018 09:40:59 -0500 Subject: * 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. --- generic/proof-script.el | 15 ++++++--------- 1 file changed, 6 insertions(+), 9 deletions(-) (limited to 'generic/proof-script.el') 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 -- cgit v1.2.3