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-syntax.el | 85 +++++++++++++++++++++++++++---------------------------- 1 file changed, 41 insertions(+), 44 deletions(-) (limited to 'coq/coq-syntax.el') diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 30f1a374..b5cd1ec2 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -20,10 +20,7 @@ ;;; Code: (eval-when-compile (require 'cl-lib)) -(require 'proof-syntax) -(require 'proof-utils) ; proof-locate-executable (require 'coq-db) -(require 'span) ;;; keyword databases @@ -1050,9 +1047,9 @@ Use ‘coq-goal-command-p’ on a span instead if possible." ;; to look at Modules and section (actually indentation will still ;; need it) (defun coq-goal-command-p (span) - (or (span-property span 'goalcmd) + (or (overlay-get span 'goalcmd) ;; module and section starts are detected here - (let ((str (or (span-property span 'cmd) ""))) + (let ((str (or (overlay-get span 'cmd) ""))) (or (coq-section-command-p str) (coq-module-opening-p str))))) @@ -1073,15 +1070,18 @@ It is used: ;; It is understood here as being a goal. This is important for ;; recognizing global identifiers, see coq-global-p. (defconst coq-save-command-regexp-strict - (proof-anchor-regexp - (concat "\\(?:Time\\s-+\\)?\\(" (proof-ids-to-regexp coq-keywords-save-strict) - "\\)"))) + (concat "\\`\\(?:Time\\s-+\\)?\\(" + "\\_<" + (regexp-opt coq-keywords-save-strict) + "\\_>" + "\\)")) (defun coq-save-command-p (_span str) "Decide whether argument is a Save command or not." - (or (proof-string-match coq-save-command-regexp-strict str) - (and (proof-string-match "\\`Proof\\_>" str) - (not (proof-string-match "\\`Proof\\s-*\\(\\.\\|\\_\\|\\_\\)" str))))) + (let ((case-fold-search nil)) + (or (string-match coq-save-command-regexp-strict str) + (and (string-match "\\`Proof\\_>" str) + (not (string-match "\\`Proof\\s-*\\(\\.\\|\\_\\|\\_\\)" str)))))) ;; ----- keywords for font-lock. @@ -1195,10 +1195,10 @@ It is used: "All keywords in a Coq script.") ;; coq-build-opt-regexp-from-db already adds "\\_<" "\\_>" -(defun proof-regexp-alt-list-symb (args) - (concat "\\_<\\(?:" (proof-regexp-alt-list args) "\\)\\_>")) +(defun coq--regexp-alt-list-symb (args) + (concat "\\_<\\(?:" (mapconcat #'identity args "\\|") "\\)\\_>")) -(defvar coq-keywords-regexp (proof-regexp-alt-list-symb coq-keywords)) +(defvar coq-keywords-regexp (coq--regexp-alt-list-symb coq-keywords)) (defvar coq-symbols @@ -1292,30 +1292,31 @@ It is used: (defconst coq-save-command-regexp - (proof-anchor-regexp - (concat "\\(?:Time\\s-+\\)?\\(" (proof-ids-to-regexp coq-keywords-save) - "\\)"))) + ;; FIXME: The surrounding grouping parens are probably not needed. + (concat "\\`\\(\\(?:Time\\s-+\\)?\\_<" + (regexp-opt coq-keywords-save t) + "\\_>\\)")) (defconst coq-save-with-hole-regexp - (concat "\\(?:Time\\s-+\\)?\\(" (proof-regexp-alt-list coq-keywords-save-strict) + (concat "\\(?:Time\\s-+\\)?\\(" (regexp-opt coq-keywords-save-strict) "\\)\\s-+\\(" coq-id "\\)\\s-*\\.")) (defconst coq-goal-command-regexp - (proof-anchor-regexp (proof-regexp-alt-list coq-keywords-goal))) + (concat "\\`\\(?:" (mapconcat #'identity coq-keywords-goal "\\|") "\\)")) (defconst coq-goal-with-hole-regexp - (concat "\\(" (proof-regexp-alt-list coq-keywords-goal) + (concat "\\(" (mapconcat #'identity coq-keywords-goal "\\|") "\\)\\s-+\\(" coq-id "\\)\\s-*:?")) (defconst coq-decl-with-hole-regexp - (concat "\\(" (proof-regexp-alt-list coq-keywords-decl) + (concat "\\(" (mapconcat #'identity coq-keywords-decl "\\|") "\\)\\s-+\\(" coq-ids "\\)\\s-*:")) ;; (defconst coq-decl-with-hole-regexp ;; (if coq-variable-highlight-enable coq-decl-with-hole-regexp-1 'nil)) (defconst coq-defn-with-hole-regexp - (concat "\\(" (proof-regexp-alt-list coq-keywords-defn) + (concat "\\(" (mapconcat #'identity coq-keywords-defn "\\|") "\\)\\s-+\\(" coq-id "\\)")) ;; must match: @@ -1346,8 +1347,8 @@ It is used: (,coq-keywords-regexp . 'font-lock-keyword-face) (,coq-reserved-regexp . 'font-lock-type-face) (,coq-tactics-regexp . 'proof-tactics-name-face) - (,(proof-regexp-alt-list coq-tacticals) . 'proof-tacticals-name-face) - (,(proof-regexp-alt-list-symb (list "Set" "Type" "Prop")) . 'font-lock-type-face) + (,(mapconcat #'identity coq-tacticals "\\|") . 'proof-tacticals-name-face) + (,(coq--regexp-alt-list-symb (list "Set" "Type" "Prop")) . 'font-lock-type-face) ("============================" . 'font-lock-keyword-face) (,coq-goal-with-hole-regexp 2 'font-lock-function-name-face) (,coq-context-marker-regexp 1 'coq-context-qualifier-face)) @@ -1382,11 +1383,10 @@ part of another hypothesis.") (concat coq-hyp-name-in-goal-or-response-regexp "\\|\\(?1:^\\s-+========\\)")) (defun coq-find-first-hyp () - (with-current-buffer proof-goals-buffer - (save-excursion - (goto-char (point-min)) - (search-forward-regexp coq-hyp-name-in-goal-or-response-regexp nil t) - (match-beginning 2)))) + (save-excursion + (goto-char (point-min)) + (search-forward-regexp coq-hyp-name-in-goal-or-response-regexp nil t) + (match-beginning 2))) (defun coq-detect-hyps-positions (buf &optional limit) "Detect all hypotheses displayed in buffer BUF and returns positions. @@ -1420,11 +1420,10 @@ part of another hypothesis.") ;; Don't look at the conclusion of the goal (defun coq-detect-hyps-positions-in-goals () - (with-current-buffer proof-goals-buffer - (goto-char (point-min)) - (coq-detect-hyps-positions - proof-goals-buffer - (if (search-forward-regexp "==========" nil t) (point) nil)))) + (goto-char (point-min)) + (coq-detect-hyps-positions + (current-buffer) + (if (search-forward-regexp "==========" nil t) (point) nil))) ;; We define a slightly different set of keywords for response buffer. @@ -1437,8 +1436,8 @@ part of another hypothesis.") (cons coq-keywords-regexp 'font-lock-keyword-face) (cons coq-shell-eager-annotation-start 'proof-warning-face) (cons coq-error-regexp 'proof-error-face) - (cons (proof-regexp-alt-list-symb (list "In environment" "The term" "has type")) 'proof-error-face) - (cons (proof-regexp-alt-list-symb (list "Set" "Type" "Prop")) 'font-lock-type-face) + (cons (coq--regexp-alt-list-symb (list "In environment" "The term" "has type")) 'proof-error-face) + (cons (coq--regexp-alt-list-symb (list "Set" "Type" "Prop")) 'font-lock-type-face) (list (concat "[?]" coq-id) 0 'coq-question-mark-face) ;; highlight evars and Ltac variables (list coq-hyp-name-in-goal-or-response-regexp 2 'proof-declaration-name-face) (list "^\\([^ \n]+\\) \\(is defined\\)" (list 1 'font-lock-function-name-face t))))) @@ -1450,21 +1449,19 @@ part of another hypothesis.") (cons coq-reserved-regexp 'font-lock-type-face) (list (concat "[?]" coq-id) 0 'coq-question-mark-face) ;; highlight evars and Ltac variables (list coq-hyp-name-in-goal-or-response-regexp 2 'proof-declaration-name-face) - (cons (proof-regexp-alt-list-symb (list "Set" "Type" "Prop")) 'font-lock-type-face)))) + (cons (coq--regexp-alt-list-symb (list "Set" "Type" "Prop")) 'font-lock-type-face)))) -;; use this to evaluate code with "." being consisdered a symbol +;; 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). (defmacro coq-with-altered-syntax-table (&rest code) (declare (debug t)) - (let ((res (make-symbol "res"))) - `(unwind-protect - (progn (modify-syntax-entry ?\. "_") - (let ((,res (progn ,@code))) - (modify-syntax-entry ?\. ".") - ,res))))) + `(unwind-protect + (progn (modify-syntax-entry ?\. "_") + ,@code) + (modify-syntax-entry ?\. "."))) (defconst coq-generic-expression (mapcar (lambda (kw) -- cgit v1.2.3