Make coq-mode work without generic/proof-*

Revise the various `require`s to avoid spurious dependencies, and tweak
the code here and there to eliminate the remaining dependencies.

* coq/coq-db.el: Don't require proof-config nor proof-syntax.
(coq-build-opt-regexp-from-db): Avoid proof-regexp-alt-list.

* coq/coq-indent.el: Use lexical-binding.  Don't require coq-syntax.
Comment out all the code that's not used any more.
(coq-empty-command-p): Use forward-comment instead of
coq-find-not-in-comment-backward.  Fix paren typos.
(coq-script-parse-cmdend-forward, coq-script-parse-cmdend-backward):
Use forward-comment i.s.o proof-script-generic-parse-find-comment-end.
Use syntax-ppss i.s.o proof-buffer-syntactic-context.
(coq-find-current-start): Explicit case-fold-search i.s.o proof-looking-at.

* coq/coq-mode.el (coq-mode): Set comment-start/end.

* coq/coq-smie.el: Require coq-syntax explicitly.
(coq-smie-detect-goal-command, coq-smie-module-deambiguate):
Explicit case-fold-search i.s.o proof-looking-at.
(coq-indent-basic): New custom var.
(coq-smie-rules): Use it in case PG is not loaded.

* coq/coq-syntax.el: Don't require proof-syntax, proof-utils, and span.
(coq-goal-command-p): Use overlay-get i.s.o span-property.
(coq-save-command-regexp-strict, coq-save-command-regexp):
Use \` and regexp-opt i.s.o proof-anchor-regexp and proof-ids-to-regexp.
(coq-save-command-p): Explicit case-fold-search i.s.o proof-string-match.
(coq--regexp-alt-list-symb): Rename from proof-regexp-alt-list-symb.
Use mapconcat i.s.o proof-regexp-alt-list.
(coq-save-with-hole-regexp): Use regexp-opt i.s.o proof-regexp-alt-list.
(coq-goal-command-regexp, coq-goal-with-hole-regexp)
(coq-decl-with-hole-regexp, coq-defn-with-hole-regexp)
(coq-font-lock-keywords-1): Use mapconcat i.s.o proof-regexp-alt-list.
(coq-find-first-hyp, coq-detect-hyps-positions-in-goals):
Use current buffer i.s.o proof-goals-buffer.
(coq-with-altered-syntax-table): Fix broken use of unwind-protect.

* coq/coq.el (coq-detect-hyps-in-goals): Change buffer before calling
coq-find-first-hyp and coq-detect-hyps-positions-in-goals.
(coq-pg-setup): Use comment-start/end.

* generic/pg-goals.el: Require proof-script explicitly instead of
autoloading via proof-insert-sendback-command.

* generic/pg-pbrpm.el: Require proof-script explicitly instead of
autoloading via proof-insert-pbp-command.

* generic/pg-pgip.el: Require proof-script explicitly.

* generic/proof-depends.el: Require proof-script explicitly instead of
autoloading via pg-set-span-helphighlights.

* generic/proof-script.el (pg-set-span-helphighlights)
(proof-insert-pbp-command, proof-insert-sendback-command)
(proof-script-generic-parse-find-comment-end): Don't autoload.

* generic/proof-syntax.el (proof-ids-to-regexp): Simplify.

* lib/span.el (span-delete): η-reduce.

1 files changed, 0 insertions, 4 deletions

diff --git a/generic/proof-script.el b/generic/proof-script.el
index aa9841f0..59b7074a 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -766,7 +766,6 @@ This is used to annotate the buffer with the result of proof steps."
 	
       text)))
 
-;;;###autoload
 (defun pg-set-span-helphighlights (span &optional mouseface face)
   "Add a daughter help span for SPAN with help message, highlight, actions.
 The daughter span covers the non whitespace content of the main span.
@@ -1763,7 +1762,6 @@ to the function which parses the script segment by segment."
       ;; Return segment list
       segs)))
 
-;;;###autoload
 (defun proof-script-generic-parse-find-comment-end ()
   "Find the end of the comment point is at the start of.  Nil if not found."
   (let ((notout t))
@@ -2049,7 +2047,6 @@ No effect if prover is busy."
 ;;
 ;; PBP call-backs
 ;;
-;;;###autoload
 (defun proof-insert-pbp-command (cmd)
   "Insert CMD into the proof queue."
   (proof-activate-scripting)
@@ -2064,7 +2061,6 @@ No effect if prover is busy."
 		       (list (list span (list cmd)
 				   'proof-done-advancing)))))
 
-;;;###autoload
 (defun proof-insert-sendback-command (cmd)
   "Insert CMD into the proof script, execute assert-until-point."
   (proof-with-script-buffer