From fb3b75dab55b6e6befffc53e136422558be5faa0 Mon Sep 17 00:00:00 2001 From: Stefan Monnier Date: Wed, 26 Dec 2018 18:00:43 -0500 Subject: Make coq-mode work without generic/proof-* MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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. --- coq/coq.el | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) (limited to 'coq/coq.el') diff --git a/coq/coq.el b/coq/coq.el index 29a6c1ad..662cc2e8 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -1464,8 +1464,10 @@ Maintained by a hook in `proof-shell-handle-delayed-output-hook'.") Three overlays are created for each hyp: (hypov hypnameov hypcrossov), respectively for the whole hyp, only its name and the overlay for fold/unfold cross. Return the list of mappings hypname -> overlays." + ;; FIXME: Consolidate the `with-current-buffer proof-goals-buffer's. (let* - ((fsthyp-pos (coq-find-first-hyp)) + ((fsthyp-pos (with-current-buffer proof-goals-buffer + (coq-find-first-hyp))) (fsthyp-ov (when fsthyp-pos (with-current-buffer proof-goals-buffer (overlays-at fsthyp-pos)))) ; is there at least one hyp overlay there? @@ -1473,7 +1475,9 @@ fold/unfold cross. Return the list of mappings hypname -> overlays." (cl-some (lambda(x) (overlay-get x 'hyp-name)) fsthyp-ov)))) (if fsthyp-hypov coq-hyps-positions ;overlays are already there - (coq-build-hyps-overlays (coq-detect-hyps-positions-in-goals) proof-goals-buffer)))) + (with-current-buffer proof-goals-buffer + (coq-build-hyps-overlays (coq-detect-hyps-positions-in-goals) + proof-goals-buffer))))) (defun coq-find-hyp-overlay (h) (cadr (assoc h coq-hyps-positions))) @@ -1856,8 +1860,8 @@ See `coq-fold-hyp'." (setq proof-terminal-string ".") (setq proof-script-command-end-regexp coq-script-command-end-regexp) (setq proof-script-parse-function 'coq-script-parse-function) - (setq proof-script-comment-start "(*") - (setq proof-script-comment-end "*)") + (setq proof-script-comment-start comment-start) + (setq proof-script-comment-end comment-end) (setq proof-script-insert-newlines nil) (setq proof-unnamed-theorem-name "Unnamed_thm") ; Coq's default name -- cgit v1.2.3