From f7cc8f1f76baf5e517e51f1db47510ed605064e8 Mon Sep 17 00:00:00 2001
From: Stefan Monnier <monnier@iro.umontreal.ca>
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-autoloads.el | 151 ++++++++++++++++++++++++++++-----------------
 1 file changed, 95 insertions(+), 56 deletions(-)

(limited to 'generic/proof-autoloads.el')

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))
 
 ;;;***
 
-- 
cgit v1.2.3