diff options
author | Stefan Monnier <monnier@iro.umontreal.ca> | 2018-12-26 18:00:43 -0500 |
---|---|---|
committer | Stefan Monnier <monnier@iro.umontreal.ca> | 2018-12-26 18:00:43 -0500 |
commit | fb3b75dab55b6e6befffc53e136422558be5faa0 (patch) | |
tree | b3ec11dfb4581ec752057b98c638ee00a6c59f41 /lib | |
parent | 7389d43893569ff0e1eff892254901876fc8225e (diff) |
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.
Diffstat (limited to 'lib')
-rw-r--r-- | lib/span.el | 17 |
1 files changed, 8 insertions, 9 deletions
diff --git a/lib/span.el b/lib/span.el index 4bb7507e..48cfb3c9 100644 --- a/lib/span.el +++ b/lib/span.el @@ -24,17 +24,17 @@ ;;; Code: -(defalias 'span-start 'overlay-start) -(defalias 'span-end 'overlay-end) -(defalias 'span-set-property 'overlay-put) -(defalias 'span-property 'overlay-get) +(defalias 'span-start #'overlay-start) +(defalias 'span-end #'overlay-end) +(defalias 'span-set-property #'overlay-put) +(defalias 'span-property #'overlay-get) (defun span-make (&rest args) (let ((span (apply #'make-overlay args))) (span-set-property span 'pg-span t) span)) -(defalias 'span-detach 'delete-overlay) -(defalias 'span-set-endpoints 'move-overlay) -(defalias 'span-buffer 'overlay-buffer) +(defalias 'span-detach #'delete-overlay) +(defalias 'span-set-endpoints #'move-overlay) +(defalias 'span-buffer #'overlay-buffer) (defun span-p (ol) "Check if an overlay OL belongs to PG." @@ -95,8 +95,7 @@ (defun span-delete (span) "Run the 'span-delete-actions and delete SPAN." - (mapc (lambda (predelfn) (funcall predelfn)) - (span-property span 'span-delete-actions)) + (mapc #'funcall (span-property span 'span-delete-actions)) (delete-overlay span)) (defun span-add-delete-action (span action) |