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

1 files changed, 0 insertions, 28 deletions

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