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-db.el | 4 +- coq/coq-indent.el | 1547 ++++++++++++++++++++++---------------------- coq/coq-mode.el | 2 + coq/coq-smie.el | 30 +- coq/coq-syntax.el | 85 ++- coq/coq.el | 12 +- generic/pg-goals.el | 1 + generic/pg-pbrpm.el | 1 + generic/pg-pgip.el | 3 +- generic/proof-autoloads.el | 117 ++-- generic/proof-depends.el | 1 + generic/proof-script.el | 4 - generic/proof-syntax.el | 4 +- lib/span.el | 17 +- 14 files changed, 902 insertions(+), 926 deletions(-) diff --git a/coq/coq-db.el b/coq/coq-db.el index 7e59bffb..b01e8018 100644 --- a/coq/coq-db.el +++ b/coq/coq-db.el @@ -25,8 +25,6 @@ (eval-when-compile (require 'cl-lib)) ;decf -(require 'proof-config) -(require 'proof-syntax) ; for proof-ids-to-regexp (require 'holes) (defconst coq-syntax-db nil @@ -162,7 +160,7 @@ regexp. See `coq-syntax-db' for DB structure." (setq l tl))) ; da: next call is wrong? ; (proof-ids-to-regexp res))) - (concat "\\_<\\(?:" (proof-regexp-alt-list res) "\\)\\_>"))) + (concat "\\_<\\(?:" (mapconcat #'identity res "\\|") "\\)\\_>"))) ;; Computes the max length of strings in a list diff --git a/coq/coq-indent.el b/coq/coq-indent.el index ba4db8c3..a8d94234 100644 --- a/coq/coq-indent.el +++ b/coq/coq-indent.el @@ -1,4 +1,4 @@ -;;; coq-indent.el --- indentation for Coq +;;; coq-indent.el --- indentation for Coq -*- lexical-binding:t -*- ;; This file is part of Proof General. @@ -24,7 +24,6 @@ ;;; Code: -(require 'coq-syntax) ;; debugging ;(defmacro measure-time (&rest body) @@ -33,78 +32,78 @@ ; ,@body ; (message "%.06f" (float-time (time-since time))))) -(defvar coq-script-indent) +;; (defvar coq-script-indent) -(defconst coq-any-command-regexp - (proof-regexp-alt-list coq-keywords)) +;; (defconst coq-any-command-regexp +;; (proof-regexp-alt-list coq-keywords)) -(defconst coq-indent-inner-regexp - (proof-regexp-alt - "[[]()]" "[^{]|[^}]" - ;; forall with must not be enclosed by \\< and - ;;\\> . "~" forall but interacts with 'not' - (proof-ids-to-regexp - '("as" "Cases" "match" "else" "Fix" "forall" "fun" "if" "into" "let" "then" - "using" "after")))) +;; (defconst coq-indent-inner-regexp +;; (proof-regexp-alt +;; "[[]()]" "[^{]|[^}]" +;; ;; forall with must not be enclosed by \\< and +;; ;;\\> . "~" forall but interacts with 'not' +;; (proof-ids-to-regexp +;; '("as" "Cases" "match" "else" "Fix" "forall" "fun" "if" "into" "let" "then" +;; "using" "after")))) ; "ALL" "True" "False" "EX" "end" "in" "of" "with" -(defconst coq-comment-start-regexp "(\\*") -(defconst coq-comment-end-regexp "\\*)") -(defconst coq-comment-start-or-end-regexp - (concat coq-comment-start-regexp "\\|" coq-comment-end-regexp)) -(defconst coq-indent-open-regexp - (proof-regexp-alt ;(proof-regexp-alt-list coq-keywords-goal) goal-command-p instead - (proof-ids-to-regexp '("Cases" "match" "BeginSubproof")) - "\\s(" "{|")) - -(defconst coq-indent-close-regexp - (proof-regexp-alt "\\s)" "|}" "}" - (proof-ids-to-regexp '("end" "EndSubProof")) - (proof-ids-to-regexp coq-keywords-save))) - - -(defconst coq-indent-closepar-regexp "\\s)") -(defconst coq-indent-closematch-regexp (proof-ids-to-regexp '("end"))) -(defconst coq-indent-openpar-regexp "\\s(") -(defconst coq-indent-openmatch-regexp (proof-ids-to-regexp '("match" "Cases"))) -(defconst coq-tacticals-tactics-regex - (proof-regexp-alt (proof-regexp-alt-list (append coq-tacticals coq-tactics)))) -(defconst coq-indent-any-regexp - (proof-regexp-alt coq-indent-close-regexp coq-indent-open-regexp - coq-indent-inner-regexp coq-any-command-regexp - coq-tacticals-tactics-regex)) -(defconst coq-indent-kw - (proof-regexp-alt-list (cons coq-any-command-regexp - (cons coq-indent-inner-regexp - (append coq-tacticals coq-tactics))))) +;; (defconst coq-comment-start-regexp "(\\*") +;; (defconst coq-comment-end-regexp "\\*)") +;; (defconst coq-comment-start-or-end-regexp +;; (concat coq-comment-start-regexp "\\|" coq-comment-end-regexp)) +;; (defconst coq-indent-open-regexp +;; (proof-regexp-alt ;(proof-regexp-alt-list coq-keywords-goal) goal-command-p instead +;; (proof-ids-to-regexp '("Cases" "match" "BeginSubproof")) +;; "\\s(" "{|")) + +;; (defconst coq-indent-close-regexp +;; (proof-regexp-alt "\\s)" "|}" "}" +;; (proof-ids-to-regexp '("end" "EndSubProof")) +;; (proof-ids-to-regexp coq-keywords-save))) + + +;; (defconst coq-indent-closepar-regexp "\\s)") +;; (defconst coq-indent-closematch-regexp (proof-ids-to-regexp '("end"))) +;; (defconst coq-indent-openpar-regexp "\\s(") +;; (defconst coq-indent-openmatch-regexp (proof-ids-to-regexp '("match" "Cases"))) +;; (defconst coq-tacticals-tactics-regex +;; (proof-regexp-alt (proof-regexp-alt-list (append coq-tacticals coq-tactics)))) +;; (defconst coq-indent-any-regexp +;; (proof-regexp-alt coq-indent-close-regexp coq-indent-open-regexp +;; coq-indent-inner-regexp coq-any-command-regexp +;; coq-tacticals-tactics-regex)) +;; (defconst coq-indent-kw +;; (proof-regexp-alt-list (cons coq-any-command-regexp +;; (cons coq-indent-inner-regexp +;; (append coq-tacticals coq-tactics))))) ; pattern matching detection, will be tested only at beginning of a ; line (only white sapces before "|") must not match "|" followed by ; another symbol the following char must not be a symbol (tokens of coq ; are the biggest symbol cocateantions) -(defconst coq-indent-pattern-regexp "\\(|\\(?:(\\|\\s-\\|\\w\\|\n\\)\\|with\\)") +;; (defconst coq-indent-pattern-regexp "\\(|\\(?:(\\|\\s-\\|\\w\\|\n\\)\\|with\\)") ;;;; End of regexps -(defun coq-indent-goal-command-p (str) - "Syntactical detection of a Coq goal opening. -Only used in indentation code and in v8.0 compatibility mode. -Module, Definition and Function need a special parsing to detect -if they start something or not." - (let* ((match (coq-count-match "\\_" str)) - (with (coq-count-match "\\_" str)) - (letwith (+ (coq-count-match "\\_" str) (- with match))) - (affect (coq-count-match ":=" str))) - - (and (proof-string-match coq-goal-command-regexp str) - (not - (and (proof-string-match "\\`\\(Definition\\|Instance\\|Lemma\\|Module\\)\\>" str) - (not (= letwith affect)))) - (not (proof-string-match "\\`Declare\\s-+Module\\(\\w\\|\\s-\\|<\\)*:" str)) - (not - (and (proof-string-match "\\`\\(Function\\|GenFixpoint\\)\\>" str) - (not (proof-string-match "{\\s-*\\(wf\\|measure\\)" str))))))) +;; (defun coq-indent-goal-command-p (str) +;; "Syntactical detection of a Coq goal opening. +;; Only used in indentation code and in v8.0 compatibility mode. +;; Module, Definition and Function need a special parsing to detect +;; if they start something or not." +;; (let* ((match (coq-count-match "\\_" str)) +;; (with (coq-count-match "\\_" str)) +;; (letwith (+ (coq-count-match "\\_" str) (- with match))) +;; (affect (coq-count-match ":=" str))) + +;; (and (proof-string-match coq-goal-command-regexp str) +;; (not +;; (and (proof-string-match "\\`\\(Definition\\|Instance\\|Lemma\\|Module\\)\\>" str) +;; (not (= letwith affect)))) +;; (not (proof-string-match "\\`Declare\\s-+Module\\(\\w\\|\\s-\\|<\\)*:" str)) +;; (not +;; (and (proof-string-match "\\`\\(Function\\|GenFixpoint\\)\\>" str) +;; (not (proof-string-match "{\\s-*\\(wf\\|measure\\)" str))))))) (defconst coq-simple-cmd-ender-prefix-regexp "[^.]\\|\\=\\|\\.\\." @@ -235,132 +234,132 @@ Remqrk: This regexp is much more precise than `coq-end-command-regexp' but only works when searching backward.") -(defun coq-search-comment-delimiter-forward () - "Search forward for a comment start (return 1) or end (return -1). -Return nil if not found." - (when (re-search-forward coq-comment-start-or-end-regexp nil 'dummy) - (save-excursion - (goto-char (match-beginning 0)) - (if (looking-at coq-comment-start-regexp) 1 -1)))) - - -(defun coq-search-comment-delimiter-backward () - "Search backward for a comment start (return 1) or end (return -1). -Return nil if not found." - (when (re-search-backward coq-comment-start-or-end-regexp nil 'dummy) - (if (looking-at coq-comment-start-regexp) 1 -1))) - - -(defun coq-skip-until-one-comment-backward () - "Skips comments and normal text until finding an unclosed comment start. -Return nil if not found. Point is moved to the the unclosed comment start -if found, to (point-max) otherwise. Return t if found, nil otherwise." - (if (= (point) (point-min)) nil - (ignore-errors (backward-char 1)) ; if point is between '(' and '*' - (if (looking-at coq-comment-start-regexp) t - (forward-char 1) - (let ((nbopen 1) (kind nil)) - (while (and (> nbopen 0) (setq kind (coq-search-comment-delimiter-backward))) - (if (< kind 0) - (setq nbopen (+ 1 nbopen)) - (setq nbopen (- nbopen 1)))) - (= nbopen 0))))) - -(defun coq-skip-until-one-comment-forward () - "Skips comments and normal text until finding an unopened comment end." - (ignore-errors (backward-char 1)) ; if point is between '*' and ')' - (if (looking-at coq-comment-end-regexp) (progn (forward-char 2) t) - (forward-char 1) - (let ((nbopen 1) (kind nil)) - (while (and (> nbopen 0) (setq kind (coq-search-comment-delimiter-forward))) - (if (> kind 0) (setq nbopen (+ 1 nbopen)) - (setq nbopen (- nbopen 1)))) - (= nbopen 0)))) - -(defun coq-looking-at-comment () - "Return non-nil if point is inside a comment." - (or (proof-inside-comment (point)) - (proof-inside-comment (+ 1 (point))))) - -(defun coq-find-comment-start () - "Go to the current comment start. -If inside nested comments, go to the start of the outer most comment. -Return the position of the comment start. If not inside a comment, -return nil and does not move the point." - (when (coq-looking-at-comment) - (let ((prevpos (point)) (init (point))) - (while (coq-skip-until-one-comment-backward) - (setq prevpos (point))) - (goto-char prevpos) - (if (= prevpos init) nil prevpos)))) - -(defun coq-find-comment-end () - "Go to the current comment end. -If inside nested comments, go to the end of the outer most -comment. Return the position of the end of comment end. If not inside -a comment, return nil and does not move the point." - (let ((prevpos (point)) (init (point))) - (while (coq-skip-until-one-comment-forward) - (setq prevpos (point))) - (goto-char prevpos) - (if (= prevpos init) nil prevpos))) +;; (defun coq-search-comment-delimiter-forward () +;; "Search forward for a comment start (return 1) or end (return -1). +;; Return nil if not found." +;; (when (re-search-forward coq-comment-start-or-end-regexp nil 'dummy) +;; (save-excursion +;; (goto-char (match-beginning 0)) +;; (if (looking-at coq-comment-start-regexp) 1 -1)))) + + +;; (defun coq-search-comment-delimiter-backward () +;; "Search backward for a comment start (return 1) or end (return -1). +;; Return nil if not found." +;; (when (re-search-backward coq-comment-start-or-end-regexp nil 'dummy) +;; (if (looking-at coq-comment-start-regexp) 1 -1))) + + +;; (defun coq-skip-until-one-comment-backward () +;; "Skips comments and normal text until finding an unclosed comment start. +;; Return nil if not found. Point is moved to the the unclosed comment start +;; if found, to (point-max) otherwise. Return t if found, nil otherwise." +;; (if (= (point) (point-min)) nil +;; (ignore-errors (backward-char 1)) ; if point is between '(' and '*' +;; (if (looking-at coq-comment-start-regexp) t +;; (forward-char 1) +;; (let ((nbopen 1) (kind nil)) +;; (while (and (> nbopen 0) (setq kind (coq-search-comment-delimiter-backward))) +;; (if (< kind 0) +;; (setq nbopen (+ 1 nbopen)) +;; (setq nbopen (- nbopen 1)))) +;; (= nbopen 0))))) + +;; (defun coq-skip-until-one-comment-forward () +;; "Skips comments and normal text until finding an unopened comment end." +;; (ignore-errors (backward-char 1)) ; if point is between '*' and ')' +;; (if (looking-at coq-comment-end-regexp) (progn (forward-char 2) t) +;; (forward-char 1) +;; (let ((nbopen 1) (kind nil)) +;; (while (and (> nbopen 0) (setq kind (coq-search-comment-delimiter-forward))) +;; (if (> kind 0) (setq nbopen (+ 1 nbopen)) +;; (setq nbopen (- nbopen 1)))) +;; (= nbopen 0)))) + +;; (defun coq-looking-at-comment () +;; "Return non-nil if point is inside a comment." +;; (or (proof-inside-comment (point)) +;; (proof-inside-comment (+ 1 (point))))) + +;; (defun coq-find-comment-start () +;; "Go to the current comment start. +;; If inside nested comments, go to the start of the outer most comment. +;; Return the position of the comment start. If not inside a comment, +;; return nil and does not move the point." +;; (when (coq-looking-at-comment) +;; (let ((prevpos (point)) (init (point))) +;; (while (coq-skip-until-one-comment-backward) +;; (setq prevpos (point))) +;; (goto-char prevpos) +;; (if (= prevpos init) nil prevpos)))) + +;; (defun coq-find-comment-end () +;; "Go to the current comment end. +;; If inside nested comments, go to the end of the outer most +;; comment. Return the position of the end of comment end. If not inside +;; a comment, return nil and does not move the point." +;; (let ((prevpos (point)) (init (point))) +;; (while (coq-skip-until-one-comment-forward) +;; (setq prevpos (point))) +;; (goto-char prevpos) +;; (if (= prevpos init) nil prevpos))) ; generic function is wrong when the point in between ( and * -(defun coq-looking-at-syntactic-context () - "See `proof-looking-at-syntactic-context'. -Use this one for coq instead of the generic one." - (if (coq-looking-at-comment) 'comment - (proof-looking-at-syntactic-context))) - -(defconst coq-end-command-or-comment-regexp - (concat coq-comment-end-regexp "\\|" coq-end-command-regexp)) - -(defconst coq-end-command-or-comment-start-regexp - (concat coq-comment-start-regexp "\\|" coq-end-command-regexp)) - -(defun coq-find-not-in-comment-backward (reg &optional lim submatch) - "Moves to the first not commented occurrence of REG found looking up. -The point is put exactly before the occurrence if SUBMATCH is nil, -otherwise the point is put before SUBMATCHnth matched -sub-expression (see `match-string'). If no occurrence is found, go as -far as possible and return nil." - (coq-find-comment-start) ; first go out of comment if inside some - (let ((found nil) (continue t) - (regexp (concat coq-comment-end-regexp "\\|" reg))) - (while (and (not found) continue) - (setq continue (re-search-backward regexp lim 'dummy)) - (when continue - (if (coq-looking-at-comment) - (progn (coq-skip-until-one-comment-backward)) - (progn (when submatch (goto-char (match-beginning submatch))) - (setq found t))))) - (when found (point)))) - - -(defun coq-find-not-in-comment-forward (reg &optional lim submatch) - "Moves to the first not commented occurrence of REG found looking down. -The point is put exactly before the occurrence if SUBMATCH is nil, -otherwise the point is put before SUBMATCHnth matched sub-expression -\(see `match-string'). If no occurrence is found, go as far as possible -and return nil." - ;; da: PATCH here for http://proofgeneral.inf.ed.ac.uk/trac/ticket/173 - ;; (nasty example). But I don't understand this code! - ;; Sometimes we're called outside of a comment here. - (if (coq-looking-at-comment) - (coq-find-comment-end)) - (let ((found nil) (continue t) - (regexp (concat coq-comment-start-regexp "\\|" reg))) - (while (and (not found) continue) - (setq continue (re-search-forward regexp lim 'dummy)) - (when continue - (goto-char (match-beginning 0)) - (if (looking-at coq-comment-start-regexp) - (progn (forward-char 2) (coq-skip-until-one-comment-forward)) - (progn (when (and submatch (match-beginning submatch)) - (goto-char (match-beginning submatch))) - (setq found t)) - ))) - (when found (point)))) +;; (defun coq-looking-at-syntactic-context () +;; "See `proof-looking-at-syntactic-context'. +;; Use this one for coq instead of the generic one." +;; (if (coq-looking-at-comment) 'comment +;; (proof-looking-at-syntactic-context))) + +;; (defconst coq-end-command-or-comment-regexp +;; (concat coq-comment-end-regexp "\\|" coq-end-command-regexp)) + +;; (defconst coq-end-command-or-comment-start-regexp +;; (concat coq-comment-start-regexp "\\|" coq-end-command-regexp)) + +;; (defun coq-find-not-in-comment-backward (reg &optional lim submatch) +;; "Moves to the first not commented occurrence of REG found looking up. +;; The point is put exactly before the occurrence if SUBMATCH is nil, +;; otherwise the point is put before SUBMATCHnth matched +;; sub-expression (see `match-string'). If no occurrence is found, go as +;; far as possible and return nil." +;; (coq-find-comment-start) ; first go out of comment if inside some +;; (let ((found nil) (continue t) +;; (regexp (concat coq-comment-end-regexp "\\|" reg))) +;; (while (and (not found) continue) +;; (setq continue (re-search-backward regexp lim 'dummy)) +;; (when continue +;; (if (coq-looking-at-comment) +;; (progn (coq-skip-until-one-comment-backward)) +;; (progn (when submatch (goto-char (match-beginning submatch))) +;; (setq found t))))) +;; (when found (point)))) + + +;; (defun coq-find-not-in-comment-forward (reg &optional lim submatch) +;; "Moves to the first not commented occurrence of REG found looking down. +;; The point is put exactly before the occurrence if SUBMATCH is nil, +;; otherwise the point is put before SUBMATCHnth matched sub-expression +;; \(see `match-string'). If no occurrence is found, go as far as possible +;; and return nil." +;; ;; da: PATCH here for http://proofgeneral.inf.ed.ac.uk/trac/ticket/173 +;; ;; (nasty example). But I don't understand this code! +;; ;; Sometimes we're called outside of a comment here. +;; (if (coq-looking-at-comment) +;; (coq-find-comment-end)) +;; (let ((found nil) (continue t) +;; (regexp (concat coq-comment-start-regexp "\\|" reg))) +;; (while (and (not found) continue) +;; (setq continue (re-search-forward regexp lim 'dummy)) +;; (when continue +;; (goto-char (match-beginning 0)) +;; (if (looking-at coq-comment-start-regexp) +;; (progn (forward-char 2) (coq-skip-until-one-comment-forward)) +;; (progn (when (and submatch (match-beginning submatch)) +;; (goto-char (match-beginning submatch))) +;; (setq found t)) +;; ))) +;; (when found (point)))) (defun coq-is-on-ending-context () @@ -375,32 +374,32 @@ and return nil." (defun coq-empty-command-p () "Test if between point and previous command is empty. Comments are ignored, of course." - (let ((end (point)) - (start (coq-find-not-in-comment-backward "[^[:space:]]"))) - ;; we must find a "." to be sure, because {O} {P} is allowed in definitions - ;; with implicits --> this function is recursive - (cond - ;; "{" can be prefixed by a goal selector (coq-8.8). - ;; TODO: looking-back is supposed to be slow. Find something else? - ((or (and (looking-at "{")(looking-back "[0-9]+\\s-*:\\s-*" nil t)) - (and (looking-at ":\\s-*{")(looking-back "[0-9]+\\s-*" nil t)) - (and (looking-at "[0-9]+:\\s-*{") nil t)) - (goto-char (match-beginning 0)); swallow goal selector - (coq-empty-command-p)) - ;; other bulleting syntax - ((looking-at "{\\|}\\|-\\|\\+\\|\\*") (coq-empty-command-p)) - ;; vernacular controls Time, Fail, Redirect, Timeout - ((or (and (looking-at "e\\>") (looking-back "\\") (looking-back "\\") (looking-back "\\ this function is recursive + (cond + ;; "{" can be prefixed by a goal selector (coq-8.8). + ;; TODO: looking-back is supposed to be slow. Find something else? + ((or (and (looking-at "{")(looking-back "[0-9]+\\s-*:\\s-*" nil t)) + (and (looking-at ":\\s-*{")(looking-back "[0-9]+\\s-*" nil t)) + (and (looking-at "[0-9]+:\\s-*{") nil t)) + (goto-char (match-beginning 0)) ; swallow goal selector + (coq-empty-command-p)) + ;; other bulleting syntax + ((looking-at "{\\|}\\|-\\|\\+\\|\\*") (coq-empty-command-p)) + ;; vernacular controls Time, Fail, Redirect, Timeout + ((or (and (looking-at "e\\>") (looking-back "\\") (looking-back "\\") (looking-back "\\ (coq-is-on-ending-context) 0) @@ -486,22 +485,21 @@ and return nil." ;; to search backward, next time we start from just ;; there, unless we are in a comment (goto-char foundbeg) - (let ((context (proof-buffer-syntactic-context))) - (and context ; if nil, just exit the while - ;;otherwise see what kind of syntactic + (let ((ppss (syntax-ppss))) + ;; If neither within a string nor a comment, just exit the + ;; loop. Otherwise see what kind of syntactic + (and (nth 8 ppss) (cond ;; jump directly out of a comment - ((eq context 'comment) - ;; is there something faster that this function? - ;; parse-partial-sexp seems slower - (setq foundbeg (coq-skip-until-one-comment-backward))) - ((eq context 'string) t) + ((nth 4 ppss) + (setq foundbeg (goto-char (nth 8 ppss)))) + ((nth 3 ppss) t) ;FIXME: Why? ;; nil captured before entering the cond (t (message "assert false")))))) (ignore-errors (goto-char foundbeg))) (if (and foundbeg (goto-char foundbeg) ; move to command end - (not (proof-buffer-syntactic-context))) + (not (nth 8 (syntax-ppss)))) ;; Found command end outside string/comment 'cmd ;; Didn't find command end @@ -513,9 +511,10 @@ and return nil." The point is put exactly after the end of previous command, or at the (point-min) if there is no previous command." (coq-script-parse-cmdend-backward) - (when - (proof-looking-at "\\.\\s-\\|{\\|}\\|\\++\\|\\*+\\|-+") - (forward-char (- (match-end 0) (match-beginning 0)))) ; else = no match found + (let ((case-fold-search nil)) + (when + (looking-at "\\.\\s-\\|{\\|}\\|\\++\\|\\*+\\|-+") + (forward-char (- (match-end 0) (match-beginning 0))))) ; else = no match found (point)) @@ -525,350 +524,350 @@ The point is put exactly before first non comment letter of the command." (coq-find-current-start) (forward-comment (point-max))) -(defun same-line (pt pt2) - (or (= (line-number-at-pos pt) (line-number-at-pos pt2)))) - -(defun coq-command-at-point (&optional nojumplines) - "Return the string of the command at point, nil if none. -Can jump line if NOJUMPLINES = nil." - (let ((initpos (point))) - (save-excursion - (let* ((st (coq-find-real-start)) ; va chercher trop loin? OUI - (linejumped (not (same-line initpos (point)))) - ;(xxx (goto-char (- (point) 1))) - (nd (or (if (coq-script-parse-cmdend-forward) (point) nil) - (- (point-max) 1)))) ; idem? - (if (and st (or (not nojumplines) (not linejumped))) - (buffer-substring st nd) - nil))))) - - -(defun coq-commands-at-line (&optional nojumplines) - "Return the string of each command at current line." - (save-excursion - ;; we must capture a "." or a "{" at start of the line. So we go at the end of - ;; previous line to have a left context to match - (let ((initpoint (point)) - (forward-char (coq-is-on-ending-context)) - (command-found (coq-command-at-point nojumplines)) - res - ) - (if command-found (coq-find-real-start)) - (while (and command-found - ;; need this second test even with nojumplines: - (same-line (point) initpoint)) - (setq res (cons command-found res)) - (if (and (coq-script-parse-cmdend-forward) - ;(ignore-errors (forward-char 1) t);to fit in the "and" - (coq-find-real-start)) - (setq command-found (coq-command-at-point nojumplines)) - (setq command-found nil) - )) - res))) - - -(defun coq-indent-only-spaces-on-line () - "Non-nil if there only spaces (or nothing) on the current line after point. -Moves point to first non space char if present, to the end of line otherwise." - (skip-chars-forward " \t" (save-excursion (end-of-line) (point))) - (eolp)) - -(defun coq-indent-find-reg (lim reg) - "Non-nil if REG occurs between point and LIM, not in a comment or string. -Point is moved at the end of the match if found, at LIM otherwise." - (let ((oldpt (point)) (limit lim) (found nil)) - (if (= limit (point)) nil - ;;swap limit and point if necessary -; (message "coq-indent-find-reg...") - (when (< limit (point)) (let ((x limit)) (setq limit (point)) (goto-char x))) - (prog1 - (coq-find-not-in-comment-forward reg limit) - (goto-char (match-end 0)))))) - - - -(defun coq-find-no-syntactic-on-line () - "Return non-nil if there is a not commented non white character on the line. -Moves point to this char or to the end of the line if not found (and -return nil in this case)." - (let ((eol (save-excursion (end-of-line) (point)))) - (back-to-indentation) - (while (and (coq-looking-at-syntactic-context) - (re-search-forward coq-comment-end-regexp eol 'dummy)) - (skip-chars-forward " \t")) - (not (eolp)))) - - - -(defun coq-back-to-indentation-prevline () - "Move point back to previous pertinent line for indentation. -Move point to the first non white space character. Returns 0 if -top of buffer was reached, 3 if inside a comment or string, 4 if -inside the {} of a record, 1 if the line found is not in the same -command as the point before the function was called, 2 -otherwise (point and previous line are in the same command, and -not inside the {} of a record)." - - (if (coq-looking-at-syntactic-context) 3 - (let ((oldpt (point)) - (topnotreached (= (forward-line -1) 0))) ;;; nil if going one line backward - ;;; is not possible - (while (and topnotreached - (not (coq-find-no-syntactic-on-line)) - ) - (setq topnotreached (= (forward-line -1) 0)) - (end-of-line) - (if (proof-looking-at-syntactic-context) - (re-search-backward coq-comment-start-regexp nil 'dummy) - )) - (back-to-indentation) - (if (not topnotreached) 0 ;; returns nil if top of buffer was reached - ;; if we are at end of a command (dot) find this command - ; if there is a "." alone on the line - (let ((pos (point))) - ;(ignore-errors (forward-char -1)) - (if (coq-script-parse-cmdend-forward oldpt) - (progn (forward-char -1) - ;; one more if "." found, no more if "{" or "}" - (when (proof-looking-at "\\.") (forward-char -1)) - (coq-find-real-start) - (back-to-indentation) - 1) - (goto-char pos) - (if (save-excursion - (and - (not (= (point) (point-min))) - (or (forward-char -1) t) - (coq-find-real-start) - (proof-looking-at-safe "Record\\|Class\\|Instance"); {struct} should not match this - (coq-indent-find-reg oldpt "{[^|]"))) - 4 - 2))))))) - - -(defun coq-find-unclosed (&optional optlvl limit openreg closereg) - "Finds the first unclosed open item (backward). -Counter starts to OPTLVL (default 1) and stops when reaching -LIMIT (default point-min)." - - (let* ((lvl (or optlvl 1)) - (open-re (if openreg - (proof-regexp-alt openreg proof-indent-open-regexp) - proof-indent-open-regexp)) - (close-re (if closereg - (proof-regexp-alt closereg proof-indent-close-regexp) - proof-indent-close-regexp)) - (both-re (proof-regexp-alt "\\`" close-re open-re)) - (nextpt (save-excursion - (proof-re-search-backward both-re)))) - (while - (and (not (= lvl 0)) - (>= nextpt (or limit (point-min))) - (not (= nextpt (point-min)))) - (goto-char nextpt) - (cond - ((proof-looking-at-syntactic-context) ()) - ;; ((proof-looking-at-safe proof-indent-close-regexp) - ;; (coq-find-unclosed 1 limit)) ;; recursive call - ((proof-looking-at-safe close-re) (setq lvl (+ lvl 1))) - ((proof-looking-at-safe open-re) (setq lvl (- lvl 1)))) - (setq nextpt (save-excursion (proof-re-search-backward both-re)))) - (if (= lvl 0) t - (goto-char (or limit (point-min))) - nil))) - - -(defun coq-find-at-same-level-zero (limit openreg) - "Move to open or openreg (first found) at same parenthesis level as point. -Returns point if found." - (let* (found - min-reached - (open-re (if openreg - (proof-regexp-alt openreg proof-indent-open-regexp) - proof-indent-open-regexp)) - (close-re proof-indent-close-regexp) - (both-re (proof-regexp-alt "\\`" close-re open-re)) - (nextpt (save-excursion - (proof-re-search-backward both-re)))) - - (while ; min-reached is set to t only after we have tested if found. - (and (not found) (not min-reached) - (>= nextpt (or limit (point-min)))) - (goto-char nextpt) - (cond - ((proof-looking-at-syntactic-context) ()) - ((proof-looking-at-safe openreg) (setq found t)) - ((proof-looking-at-safe proof-indent-open-regexp) (setq found t));assert false? - ;; ((proof-looking-at-safe closereg) (coq-find-unclosed 1 limit)) - ((proof-looking-at-safe proof-indent-close-regexp) - (coq-find-unclosed 1 limit))) - (if (= nextpt (point-min)) (setq min-reached t)) - (setq nextpt (save-excursion (proof-re-search-backward both-re)))) - (if found (point) nil))) - - -(defun coq-find-unopened (&optional optlvl limit) - "Find the last unopened close item (looking forward from point). -Counter starts to OPTLVL (default 1) and stops when reaching -LIMIT (default ‘point-max’). This function only works inside an -expression." - - (let ((lvl (or optlvl 1)) after nextpt endpt) - (save-excursion - (proof-re-search-forward - (proof-regexp-alt "\\'" - proof-indent-close-regexp - proof-indent-open-regexp)) - (setq after (point)) - (goto-char (match-beginning 0)) - (setq nextpt (point))) - (while - (and (not (= lvl 0)) - (<= nextpt (or limit (point-max))) - (not (= nextpt (point-max)))) - (goto-char nextpt) - (setq endpt (point)) - (cond - ((proof-looking-at-syntactic-context) ()) - - ((proof-looking-at-safe proof-indent-close-regexp) - (setq lvl (- lvl 1))) - - ((proof-looking-at-safe proof-indent-open-regexp) - (setq lvl (+ lvl 1)))) - - (goto-char after) - (save-excursion - (proof-re-search-forward - (proof-regexp-alt "\\'" - proof-indent-close-regexp - proof-indent-open-regexp)) - (setq after (point)) - (goto-char (match-beginning 0)) - (setq nextpt (point)))) - (if (= lvl 0) - (goto-char endpt) - (goto-char (or limit (point-max))) - nil))) - - - -(defun coq-find-last-unopened (&optional optlvl limit) - "Backward move to and return the point of the last close item, not opened after LIMIT." - (let ((last nil)) - (while (coq-find-unopened optlvl limit) - (setq last (point)) - (forward-char 1)); shift one to the right, - ; that way the current match won'tbe matched again - (if last (goto-char last)) - last)) - - -(defun coq-end-offset (&optional limit) - "Find the first unclosed open indent item, and return its column. -Stop when reaching LIMIT (default to ‘point-min’)." - (save-excursion - (let ((found nil) - (anyreg (proof-regexp-alt "\\`" proof-indent-any-regexp))) - (while - (and (not found) - (> (point) (or limit (point-min)))) - (proof-re-search-backward anyreg) - (cond - ((proof-looking-at-syntactic-context) ()) - - ((proof-looking-at-safe proof-indent-close-regexp) - (coq-find-unclosed)) - - ((proof-looking-at-safe proof-indent-open-regexp) - (setq found t)) - - (t ()))) - - (if found (current-column) - -1000) ; no unclosed found - ))) - - -(defun coq-add-iter (l f) - (if (eq l nil) 0 (+ (if (funcall f (car l)) 1 0) (coq-add-iter (cdr l) f)))) - -(defun coq-goal-count (l) (coq-add-iter l 'coq-indent-goal-command-p)) - -(defun coq-save-count (l) - (coq-add-iter l (lambda (x) - (or (coq-save-command-p nil x) - (eq (proof-string-match "\\<\\(?:EndSubproof\\)\\>\\|}" x) 0))))) - -(defun coq-proof-count (l) - (coq-add-iter l (lambda (x) - (eq (proof-string-match "\\<\\(?:Proof\\|BeginSubproof\\)\\>\\|{" x) 0)))) +;; (defun same-line (pt pt2) +;; (or (= (line-number-at-pos pt) (line-number-at-pos pt2)))) + +;; (defun coq-command-at-point (&optional nojumplines) +;; "Return the string of the command at point, nil if none. +;; Can jump line if NOJUMPLINES = nil." +;; (let ((initpos (point))) +;; (save-excursion +;; (let* ((st (coq-find-real-start)) ; va chercher trop loin? OUI +;; (linejumped (not (same-line initpos (point)))) +;; ;(xxx (goto-char (- (point) 1))) +;; (nd (or (if (coq-script-parse-cmdend-forward) (point) nil) +;; (- (point-max) 1)))) ; idem? +;; (if (and st (or (not nojumplines) (not linejumped))) +;; (buffer-substring st nd) +;; nil))))) + + +;; (defun coq-commands-at-line (&optional nojumplines) +;; "Return the string of each command at current line." +;; (save-excursion +;; ;; we must capture a "." or a "{" at start of the line. So we go at the end of +;; ;; previous line to have a left context to match +;; (let ((initpoint (point)) +;; (forward-char (coq-is-on-ending-context)) +;; (command-found (coq-command-at-point nojumplines)) +;; res +;; ) +;; (if command-found (coq-find-real-start)) +;; (while (and command-found +;; ;; need this second test even with nojumplines: +;; (same-line (point) initpoint)) +;; (setq res (cons command-found res)) +;; (if (and (coq-script-parse-cmdend-forward) +;; ;(ignore-errors (forward-char 1) t);to fit in the "and" +;; (coq-find-real-start)) +;; (setq command-found (coq-command-at-point nojumplines)) +;; (setq command-found nil) +;; )) +;; res))) + + +;; (defun coq-indent-only-spaces-on-line () +;; "Non-nil if there only spaces (or nothing) on the current line after point. +;; Moves point to first non space char if present, to the end of line otherwise." +;; (skip-chars-forward " \t" (save-excursion (end-of-line) (point))) +;; (eolp)) + +;; (defun coq-indent-find-reg (lim reg) +;; "Non-nil if REG occurs between point and LIM, not in a comment or string. +;; Point is moved at the end of the match if found, at LIM otherwise." +;; (let ((oldpt (point)) (limit lim) (found nil)) +;; (if (= limit (point)) nil +;; ;;swap limit and point if necessary +;; ; (message "coq-indent-find-reg...") +;; (when (< limit (point)) (let ((x limit)) (setq limit (point)) (goto-char x))) +;; (prog1 +;; (coq-find-not-in-comment-forward reg limit) +;; (goto-char (match-end 0)))))) + + + +;; (defun coq-find-no-syntactic-on-line () +;; "Return non-nil if there is a not commented non white character on the line. +;; Moves point to this char or to the end of the line if not found (and +;; return nil in this case)." +;; (let ((eol (save-excursion (end-of-line) (point)))) +;; (back-to-indentation) +;; (while (and (coq-looking-at-syntactic-context) +;; (re-search-forward coq-comment-end-regexp eol 'dummy)) +;; (skip-chars-forward " \t")) +;; (not (eolp)))) + + + +;; (defun coq-back-to-indentation-prevline () +;; "Move point back to previous pertinent line for indentation. +;; Move point to the first non white space character. Returns 0 if +;; top of buffer was reached, 3 if inside a comment or string, 4 if +;; inside the {} of a record, 1 if the line found is not in the same +;; command as the point before the function was called, 2 +;; otherwise (point and previous line are in the same command, and +;; not inside the {} of a record)." + +;; (if (coq-looking-at-syntactic-context) 3 +;; (let ((oldpt (point)) +;; (topnotreached (= (forward-line -1) 0))) ;;; nil if going one line backward +;; ;;; is not possible +;; (while (and topnotreached +;; (not (coq-find-no-syntactic-on-line)) +;; ) +;; (setq topnotreached (= (forward-line -1) 0)) +;; (end-of-line) +;; (if (proof-looking-at-syntactic-context) +;; (re-search-backward coq-comment-start-regexp nil 'dummy) +;; )) +;; (back-to-indentation) +;; (if (not topnotreached) 0 ;; returns nil if top of buffer was reached +;; ;; if we are at end of a command (dot) find this command +;; ; if there is a "." alone on the line +;; (let ((pos (point))) +;; ;(ignore-errors (forward-char -1)) +;; (if (coq-script-parse-cmdend-forward oldpt) +;; (progn (forward-char -1) +;; ;; one more if "." found, no more if "{" or "}" +;; (when (proof-looking-at "\\.") (forward-char -1)) +;; (coq-find-real-start) +;; (back-to-indentation) +;; 1) +;; (goto-char pos) +;; (if (save-excursion +;; (and +;; (not (= (point) (point-min))) +;; (or (forward-char -1) t) +;; (coq-find-real-start) +;; (proof-looking-at-safe "Record\\|Class\\|Instance"); {struct} should not match this +;; (coq-indent-find-reg oldpt "{[^|]"))) +;; 4 +;; 2))))))) + + +;; (defun coq-find-unclosed (&optional optlvl limit openreg closereg) +;; "Finds the first unclosed open item (backward). +;; Counter starts to OPTLVL (default 1) and stops when reaching +;; LIMIT (default point-min)." + +;; (let* ((lvl (or optlvl 1)) +;; (open-re (if openreg +;; (proof-regexp-alt openreg proof-indent-open-regexp) +;; proof-indent-open-regexp)) +;; (close-re (if closereg +;; (proof-regexp-alt closereg proof-indent-close-regexp) +;; proof-indent-close-regexp)) +;; (both-re (proof-regexp-alt "\\`" close-re open-re)) +;; (nextpt (save-excursion +;; (proof-re-search-backward both-re)))) +;; (while +;; (and (not (= lvl 0)) +;; (>= nextpt (or limit (point-min))) +;; (not (= nextpt (point-min)))) +;; (goto-char nextpt) +;; (cond +;; ((proof-looking-at-syntactic-context) ()) +;; ;; ((proof-looking-at-safe proof-indent-close-regexp) +;; ;; (coq-find-unclosed 1 limit)) ;; recursive call +;; ((proof-looking-at-safe close-re) (setq lvl (+ lvl 1))) +;; ((proof-looking-at-safe open-re) (setq lvl (- lvl 1)))) +;; (setq nextpt (save-excursion (proof-re-search-backward both-re)))) +;; (if (= lvl 0) t +;; (goto-char (or limit (point-min))) +;; nil))) + + +;; (defun coq-find-at-same-level-zero (limit openreg) +;; "Move to open or openreg (first found) at same parenthesis level as point. +;; Returns point if found." +;; (let* (found +;; min-reached +;; (open-re (if openreg +;; (proof-regexp-alt openreg proof-indent-open-regexp) +;; proof-indent-open-regexp)) +;; (close-re proof-indent-close-regexp) +;; (both-re (proof-regexp-alt "\\`" close-re open-re)) +;; (nextpt (save-excursion +;; (proof-re-search-backward both-re)))) + +;; (while ; min-reached is set to t only after we have tested if found. +;; (and (not found) (not min-reached) +;; (>= nextpt (or limit (point-min)))) +;; (goto-char nextpt) +;; (cond +;; ((proof-looking-at-syntactic-context) ()) +;; ((proof-looking-at-safe openreg) (setq found t)) +;; ((proof-looking-at-safe proof-indent-open-regexp) (setq found t));assert false? +;; ;; ((proof-looking-at-safe closereg) (coq-find-unclosed 1 limit)) +;; ((proof-looking-at-safe proof-indent-close-regexp) +;; (coq-find-unclosed 1 limit))) +;; (if (= nextpt (point-min)) (setq min-reached t)) +;; (setq nextpt (save-excursion (proof-re-search-backward both-re)))) +;; (if found (point) nil))) + + +;; (defun coq-find-unopened (&optional optlvl limit) +;; "Find the last unopened close item (looking forward from point). +;; Counter starts to OPTLVL (default 1) and stops when reaching +;; LIMIT (default ‘point-max’). This function only works inside an +;; expression." + +;; (let ((lvl (or optlvl 1)) after nextpt endpt) +;; (save-excursion +;; (proof-re-search-forward +;; (proof-regexp-alt "\\'" +;; proof-indent-close-regexp +;; proof-indent-open-regexp)) +;; (setq after (point)) +;; (goto-char (match-beginning 0)) +;; (setq nextpt (point))) +;; (while +;; (and (not (= lvl 0)) +;; (<= nextpt (or limit (point-max))) +;; (not (= nextpt (point-max)))) +;; (goto-char nextpt) +;; (setq endpt (point)) +;; (cond +;; ((proof-looking-at-syntactic-context) ()) + +;; ((proof-looking-at-safe proof-indent-close-regexp) +;; (setq lvl (- lvl 1))) + +;; ((proof-looking-at-safe proof-indent-open-regexp) +;; (setq lvl (+ lvl 1)))) + +;; (goto-char after) +;; (save-excursion +;; (proof-re-search-forward +;; (proof-regexp-alt "\\'" +;; proof-indent-close-regexp +;; proof-indent-open-regexp)) +;; (setq after (point)) +;; (goto-char (match-beginning 0)) +;; (setq nextpt (point)))) +;; (if (= lvl 0) +;; (goto-char endpt) +;; (goto-char (or limit (point-max))) +;; nil))) + + + +;; (defun coq-find-last-unopened (&optional optlvl limit) +;; "Backward move to and return the point of the last close item, not opened after LIMIT." +;; (let ((last nil)) +;; (while (coq-find-unopened optlvl limit) +;; (setq last (point)) +;; (forward-char 1)); shift one to the right, +;; ; that way the current match won'tbe matched again +;; (if last (goto-char last)) +;; last)) + + +;; (defun coq-end-offset (&optional limit) +;; "Find the first unclosed open indent item, and return its column. +;; Stop when reaching LIMIT (default to ‘point-min’)." +;; (save-excursion +;; (let ((found nil) +;; (anyreg (proof-regexp-alt "\\`" proof-indent-any-regexp))) +;; (while +;; (and (not found) +;; (> (point) (or limit (point-min)))) +;; (proof-re-search-backward anyreg) +;; (cond +;; ((proof-looking-at-syntactic-context) ()) + +;; ((proof-looking-at-safe proof-indent-close-regexp) +;; (coq-find-unclosed)) + +;; ((proof-looking-at-safe proof-indent-open-regexp) +;; (setq found t)) + +;; (t ()))) + +;; (if found (current-column) +;; -1000) ; no unclosed found +;; ))) + + +;; (defun coq-add-iter (l f) +;; (if (eq l nil) 0 (+ (if (funcall f (car l)) 1 0) (coq-add-iter (cdr l) f)))) + +;; (defun coq-goal-count (l) (coq-add-iter l 'coq-indent-goal-command-p)) + +;; (defun coq-save-count (l) +;; (coq-add-iter l (lambda (x) +;; (or (coq-save-command-p nil x) +;; (eq (proof-string-match "\\<\\(?:EndSubproof\\)\\>\\|}" x) 0))))) + +;; (defun coq-proof-count (l) +;; (coq-add-iter l (lambda (x) +;; (eq (proof-string-match "\\<\\(?:Proof\\|BeginSubproof\\)\\>\\|{" x) 0)))) ;; returns the difference between goal (and assimilate Proof and BeginSubproof) and ;; save commands in a commands list. This is to -(defun coq-goal-save-diff-maybe-proof (l) - (let ((proofs (coq-proof-count l)) - (saves (coq-save-count l)) - (goals (coq-goal-count l))) -; (if (= goals 0) (- (if (<= proofs 0) 0 1) (coq-save-count l)) -; (- goals (coq-save-count l))) - (- (+ proofs goals) saves) - )) - - -(defun coq-indent-command-offset (kind prevcol prevpoint) - "Return the indentation offset of the current line. -This function indents a *command* line (the first line of a command). -Use `coq-indent-expr-offset' to indent a line belonging to an expression." - (let ((diff-goal-save-current - (coq-goal-save-diff-maybe-proof (coq-commands-at-line t))) - (diff-goal-save-prev - (save-excursion - (goto-char prevpoint) - (coq-goal-save-diff-maybe-proof (coq-commands-at-line t)))) - (prev-closing-beginning ; t if the closing is at start of the (prev) line - (save-excursion - (goto-char prevpoint) - (back-to-indentation) - ;(forward-char -1) - (looking-at coq-indent-close-regexp))) - (current-closing-beginning ; t if the closing is at start of the (current) line - (save-excursion - (back-to-indentation) - (looking-at coq-indent-close-regexp)))) - ;(message "currentkind,prevcol,prevpoint = %d , %d ,%d " kind prevcol prevpoint) - (cond - ((proof-looking-at-safe "\\") 0);; no indentation at "Proof ..." - - (t (* proof-indent - (let ((res - (let ((a diff-goal-save-prev) (b diff-goal-save-current) - (a2 prev-closing-beginning) (b2 current-closing-beginning)) - ;(message "a,b,a2,b2 = %d,%d,%S,%S" a b a2 b2) - (cond - ((and (>= a 0) (>= b 0)) a) - ((and (>= a 0) (< b 0) b2) (+ a -1)) ; a + b - ((and (>= a 0) (< b 0) (not b2)) a) - ((and (< a 0) (< b 0) a2 b2) a) ; a +1 -1 - ((and (< a 0) (< b 0) a2 (not b2)) (+ a 1)) - ((and (< a 0) (< b 0) (not a2) b2) (+ a -1)) - ((and (< a 0) (< b 0) (not a2) (not b2)) a) - ((and (< a 0) (>= b 0) a2) (+ a 1)) - ((and (< a 0) (>= b 0) (not a2)) a) - (t (error "Muh?")))))) - ;(message "RES = %S" res) - ;(message "********************") - res)) - ) - ;; ;; we are at an end command -> one ident left unless previous line is a goal - ;; ;; (if goal and save are consecutive, then no indentation at all) - ;; ((and (< diff-goal-save-current 0) (<= diff-goal-save-prev 0)) (- proof-indent)) - ;; ;; previous command is a goal command -> one indent right unless the current one - ;; ;; is an end (consecutive goal and save). - ;; ((and (>= diff-goal-save-current 0) (> diff-goal-save-prev 0)) proof-indent) - ;; ;; otherwise -> same indent as previous command - ;; (t 0) - ))) +;; (defun coq-goal-save-diff-maybe-proof (l) +;; (let ((proofs (coq-proof-count l)) +;; (saves (coq-save-count l)) +;; (goals (coq-goal-count l))) +;; ; (if (= goals 0) (- (if (<= proofs 0) 0 1) (coq-save-count l)) +;; ; (- goals (coq-save-count l))) +;; (- (+ proofs goals) saves) +;; )) + + +;; (defun coq-indent-command-offset (kind prevcol prevpoint) +;; "Return the indentation offset of the current line. +;; This function indents a *command* line (the first line of a command). +;; Use `coq-indent-expr-offset' to indent a line belonging to an expression." +;; (let ((diff-goal-save-current +;; (coq-goal-save-diff-maybe-proof (coq-commands-at-line t))) +;; (diff-goal-save-prev +;; (save-excursion +;; (goto-char prevpoint) +;; (coq-goal-save-diff-maybe-proof (coq-commands-at-line t)))) +;; (prev-closing-beginning ; t if the closing is at start of the (prev) line +;; (save-excursion +;; (goto-char prevpoint) +;; (back-to-indentation) +;; ;(forward-char -1) +;; (looking-at coq-indent-close-regexp))) +;; (current-closing-beginning ; t if the closing is at start of the (current) line +;; (save-excursion +;; (back-to-indentation) +;; (looking-at coq-indent-close-regexp)))) +;; ;(message "currentkind,prevcol,prevpoint = %d , %d ,%d " kind prevcol prevpoint) +;; (cond +;; ((proof-looking-at-safe "\\") 0);; no indentation at "Proof ..." + +;; (t (* proof-indent +;; (let ((res +;; (let ((a diff-goal-save-prev) (b diff-goal-save-current) +;; (a2 prev-closing-beginning) (b2 current-closing-beginning)) +;; ;(message "a,b,a2,b2 = %d,%d,%S,%S" a b a2 b2) +;; (cond +;; ((and (>= a 0) (>= b 0)) a) +;; ((and (>= a 0) (< b 0) b2) (+ a -1)) ; a + b +;; ((and (>= a 0) (< b 0) (not b2)) a) +;; ((and (< a 0) (< b 0) a2 b2) a) ; a +1 -1 +;; ((and (< a 0) (< b 0) a2 (not b2)) (+ a 1)) +;; ((and (< a 0) (< b 0) (not a2) b2) (+ a -1)) +;; ((and (< a 0) (< b 0) (not a2) (not b2)) a) +;; ((and (< a 0) (>= b 0) a2) (+ a 1)) +;; ((and (< a 0) (>= b 0) (not a2)) a) +;; (t (error "Muh?")))))) +;; ;(message "RES = %S" res) +;; ;(message "********************") +;; res)) +;; ) +;; ;; ;; we are at an end command -> one ident left unless previous line is a goal +;; ;; ;; (if goal and save are consecutive, then no indentation at all) +;; ;; ((and (< diff-goal-save-current 0) (<= diff-goal-save-prev 0)) (- proof-indent)) +;; ;; ;; previous command is a goal command -> one indent right unless the current one +;; ;; ;; is an end (consecutive goal and save). +;; ;; ((and (>= diff-goal-save-current 0) (> diff-goal-save-prev 0)) proof-indent) +;; ;; ;; otherwise -> same indent as previous command +;; ;; (t 0) +;; ))) @@ -882,210 +881,210 @@ Use `coq-indent-expr-offset' to indent a line belonging to an expression." ;; is the indentation point of previous line, record tells if we are ;; inside the accolades of a record. -(defun coq-indent-expr-offset (kind prevcol prevpoint record) - "Return the indentation column of the current line. -This function indents a *expression* line (a line inside of a -command). Use `coq-indent-command-offset' to indent a line belonging -to a command. The fourth argument RECORD must be t if inside the {}s -of a record, nil otherwise." - ;(message "COQ-INDENT-EXPR-OFFSET") - (let ((pt (point)) real-start) - (save-excursion - (setq real-start (coq-find-real-start))) - - (cond - - ;; at a ) -> same indent as the *line* of corresponding ( - ((proof-looking-at-safe coq-indent-closepar-regexp) - (save-excursion (coq-find-unclosed 1 real-start) - (back-to-indentation) - (current-column))) - - ;; at an end -> same indent as the corresponding match or Case - ((proof-looking-at-safe coq-indent-closematch-regexp) - (save-excursion (coq-find-unclosed 1 real-start) - (current-column))) - - ;; if we find a "|" we indent from the first unclosed - ;; or from the command start (if we are in an Inductive type) - ((proof-looking-at-safe coq-indent-pattern-regexp) - (save-excursion - (coq-find-unclosed 1 real-start) - (cond - ((proof-looking-at-safe "\\s(") - (+ (current-indentation) proof-indent)) - ((proof-looking-at-safe (proof-regexp-alt-list coq-keywords-defn)) - (current-column)) - (t (+ (current-column) proof-indent))))) - - ;; if we find a "then" we indent from the first unclosed if - ;; or from the command start (should not happen) - ((proof-looking-at-safe "\\") - (save-excursion - (coq-find-unclosed 1 real-start "\\" "\\") - (back-to-indentation) - (+ (current-column) proof-indent))) - - ;; if we find a "else" we indent from the first unclosed if - ;; or from the command start (should not happen) - ((proof-looking-at-safe "\\") - (save-excursion - (coq-find-unclosed 1 real-start "\\" "\\") - (coq-find-unclosed 1 real-start "\\" "\\") - (back-to-indentation) - (+ (current-column) proof-indent))) - - ;; there is an unclosed open in the previous line - ;; -> same column if match - ;; -> same indent than prev line + indent if ( - ((coq-find-unclosed 1 prevpoint - coq-indent-openmatch-regexp - coq-indent-closematch-regexp) - (let ((base (if (proof-looking-at-safe coq-indent-openmatch-regexp) - (current-column) - prevcol))) - (+ base proof-indent))) - - -;; there is an unclosed '(' in the previous line -> prev line indent + indent -;; ((and (goto-char pt) nil)) ; just for side effect: jump to initial point -;; ((coq-find-unclosed 1 prevpoint -;; coq-indent-openpar-regexp -;; coq-indent-closepar-regexp) -;; (+ prevcol proof-indent)) - - ((and (goto-char prevpoint) nil)) ; just for side effect: jump to previous line - - ;; find the last unopened ) -> indentation of line + indent - ((coq-find-last-unopened 1 pt) ; side effect, nil if no unopenned found - (save-excursion - (coq-find-unclosed 1 real-start) - (back-to-indentation) - (current-column))) - - ;; just for side effect: jumps to end of previous line - ((and (goto-char prevpoint) - (or (and (end-of-line) nil) - (and (coq-find-not-in-comment-backward "[^[:space:]]") t)) nil)) - - ;; TODO fix with new use of { for tactics enclosing - ;; should be ok if record is ok. - ((and (proof-looking-at-safe ";") ;prev line has ";" at the end - record) ; and we are inside {}s of a record - (save-excursion - (coq-find-unclosed 1 real-start) - (back-to-indentation) - (+ (current-column) proof-indent))) - - ;; just for side effect: jumps to end of previous line - ((and (goto-char prevpoint) (not (= (coq-back-to-indentation-prevline) 0)) - (or (and (end-of-line) nil) - (and (forward-char -1) t)) nil)) - - ((and (proof-looking-at-safe ";") ;prev prev line has ";" at the end - record) ; and we are inside {}s of a record - (save-excursion (+ prevcol proof-indent))) - - ((and (goto-char pt) nil)) ;; just for side effect: go back to initial point - - ;; There is a indent keyword (fun, forall etc) - ;; and we are not in {}s of a record just after a ";" - ((coq-find-at-same-level-zero prevpoint coq-indent-kw) - ;(message "COQ-INDENT-KW") - (+ prevcol proof-indent)) - - ((and (goto-char prevpoint) nil)) ;; just for side effect: go back to previous line - ;; "|" at previous line - ((proof-looking-at-safe coq-indent-pattern-regexp) - (+ prevcol proof-indent)) - - (t prevcol)))) - - -(defun coq-indent-comment-offset () - (save-excursion - (back-to-indentation) - (let ((oldpt (point)) - ;; atstart is true if the line to indent starts with a comment start - (atstart (proof-looking-at coq-comment-start-regexp))) - ;; go back looking for a non empty line - (if (/= (forward-line -1) 0) 0 ; we are at beginning of buffer - ;; only-space on a non empty line moves the point to first non space char - (while (and (coq-indent-only-spaces-on-line) (= (forward-line -1) 0)) ()) - ;; now we found the previous non empty line - (let ((eol (save-excursion (end-of-line) (point)))) - (cond - ;; The previous line contains is the comment start - ((and (not atstart) (string-match coq-comment-start-regexp - (buffer-substring (point) eol))) - (re-search-forward coq-comment-start-regexp) ;first '(*' in the line? - (+ 1 (current-column))) - - ;; the previous is in the same comment start or a comment started at that line - ((and (not atstart) (proof-looking-at-syntactic-context)) - (skip-chars-forward " \t") - (current-column)) - - ;;we were at the first line of a comment and the current line is the - ;;previous one - (t (goto-char oldpt) - (coq-script-parse-cmdend-backward) - (coq-find-real-start) - (current-column)))))))) - - -(defun coq-indent-offset (&optional notcomments) - (let (kind prevcol prevpoint) - (save-excursion - (setq kind (coq-back-to-indentation-prevline) ;go to previous *command* (assert) - prevcol (current-column) - prevpoint (point))) - ;(message "coq-indent-offset... kind = %s ; prevcol = %s; prevpoint = %s" kind prevcol prevpoint) - (cond - ((= kind 0) 0 ; top of the buffer reached - ) - ((= kind 1) ; we are at the command level - (+ prevcol (coq-indent-command-offset kind prevcol prevpoint))) - ((= kind 2) ; we are at the expression level - (coq-indent-expr-offset kind prevcol prevpoint nil)) - ((= kind 4) ; we are at the expression level inside {}s of a record - (coq-indent-expr-offset kind prevcol prevpoint t)) - ((= kind 3) - (if notcomments nil (coq-indent-comment-offset)))))) - -(defun coq-indent-calculate (&optional notcomments) - (coq-indent-offset notcomments)) - -(defun coq-indent-line () - "Indent current line of proof script, if indentation enabled." - (interactive) - (unless (not coq-script-indent) - (save-excursion - (let ((ind (save-excursion (back-to-indentation) (coq-indent-calculate)))) - (indent-line-to (max 0 ind)))) - (if (< (current-column) (current-indentation)) - (back-to-indentation)))) - -(defun coq-indent-line-not-comments () - "Same as `coq-indent-line' but comments are not indented." - (interactive) - (unless (not coq-script-indent) - (save-excursion - (let ((ind (save-excursion (back-to-indentation) (coq-indent-calculate t)))) - (when ind (indent-line-to (max 0 ind))))) - (if (< (current-column) (current-indentation)) - (back-to-indentation)))) - -(defun coq-indent-region (start end) - (let ((deb (min start end)) (fin (max start end))) - (goto-char end) - (setq fin (point-marker)) ;; to go back there even if shifted - (goto-char deb) - (while (< (point) fin) - (or (and (bolp) (eolp)) - (coq-indent-line-not-comments)) - (forward-line 1)) - (goto-char fin))) +;; (defun coq-indent-expr-offset (kind prevcol prevpoint record) +;; "Return the indentation column of the current line. +;; This function indents a *expression* line (a line inside of a +;; command). Use `coq-indent-command-offset' to indent a line belonging +;; to a command. The fourth argument RECORD must be t if inside the {}s +;; of a record, nil otherwise." +;; ;(message "COQ-INDENT-EXPR-OFFSET") +;; (let ((pt (point)) real-start) +;; (save-excursion +;; (setq real-start (coq-find-real-start))) + +;; (cond + +;; ;; at a ) -> same indent as the *line* of corresponding ( +;; ((proof-looking-at-safe coq-indent-closepar-regexp) +;; (save-excursion (coq-find-unclosed 1 real-start) +;; (back-to-indentation) +;; (current-column))) + +;; ;; at an end -> same indent as the corresponding match or Case +;; ((proof-looking-at-safe coq-indent-closematch-regexp) +;; (save-excursion (coq-find-unclosed 1 real-start) +;; (current-column))) + +;; ;; if we find a "|" we indent from the first unclosed +;; ;; or from the command start (if we are in an Inductive type) +;; ((proof-looking-at-safe coq-indent-pattern-regexp) +;; (save-excursion +;; (coq-find-unclosed 1 real-start) +;; (cond +;; ((proof-looking-at-safe "\\s(") +;; (+ (current-indentation) proof-indent)) +;; ((proof-looking-at-safe (proof-regexp-alt-list coq-keywords-defn)) +;; (current-column)) +;; (t (+ (current-column) proof-indent))))) + +;; ;; if we find a "then" we indent from the first unclosed if +;; ;; or from the command start (should not happen) +;; ((proof-looking-at-safe "\\") +;; (save-excursion +;; (coq-find-unclosed 1 real-start "\\" "\\") +;; (back-to-indentation) +;; (+ (current-column) proof-indent))) + +;; ;; if we find a "else" we indent from the first unclosed if +;; ;; or from the command start (should not happen) +;; ((proof-looking-at-safe "\\") +;; (save-excursion +;; (coq-find-unclosed 1 real-start "\\" "\\") +;; (coq-find-unclosed 1 real-start "\\" "\\") +;; (back-to-indentation) +;; (+ (current-column) proof-indent))) + +;; ;; there is an unclosed open in the previous line +;; ;; -> same column if match +;; ;; -> same indent than prev line + indent if ( +;; ((coq-find-unclosed 1 prevpoint +;; coq-indent-openmatch-regexp +;; coq-indent-closematch-regexp) +;; (let ((base (if (proof-looking-at-safe coq-indent-openmatch-regexp) +;; (current-column) +;; prevcol))) +;; (+ base proof-indent))) + + +;; ;; there is an unclosed '(' in the previous line -> prev line indent + indent +;; ;; ((and (goto-char pt) nil)) ; just for side effect: jump to initial point +;; ;; ((coq-find-unclosed 1 prevpoint +;; ;; coq-indent-openpar-regexp +;; ;; coq-indent-closepar-regexp) +;; ;; (+ prevcol proof-indent)) + +;; ((and (goto-char prevpoint) nil)) ; just for side effect: jump to previous line + +;; ;; find the last unopened ) -> indentation of line + indent +;; ((coq-find-last-unopened 1 pt) ; side effect, nil if no unopenned found +;; (save-excursion +;; (coq-find-unclosed 1 real-start) +;; (back-to-indentation) +;; (current-column))) + +;; ;; just for side effect: jumps to end of previous line +;; ((and (goto-char prevpoint) +;; (or (and (end-of-line) nil) +;; (and (coq-find-not-in-comment-backward "[^[:space:]]") t)) nil)) + +;; ;; TODO fix with new use of { for tactics enclosing +;; ;; should be ok if record is ok. +;; ((and (proof-looking-at-safe ";") ;prev line has ";" at the end +;; record) ; and we are inside {}s of a record +;; (save-excursion +;; (coq-find-unclosed 1 real-start) +;; (back-to-indentation) +;; (+ (current-column) proof-indent))) + +;; ;; just for side effect: jumps to end of previous line +;; ((and (goto-char prevpoint) (not (= (coq-back-to-indentation-prevline) 0)) +;; (or (and (end-of-line) nil) +;; (and (forward-char -1) t)) nil)) + +;; ((and (proof-looking-at-safe ";") ;prev prev line has ";" at the end +;; record) ; and we are inside {}s of a record +;; (save-excursion (+ prevcol proof-indent))) + +;; ((and (goto-char pt) nil)) ;; just for side effect: go back to initial point + +;; ;; There is a indent keyword (fun, forall etc) +;; ;; and we are not in {}s of a record just after a ";" +;; ((coq-find-at-same-level-zero prevpoint coq-indent-kw) +;; ;(message "COQ-INDENT-KW") +;; (+ prevcol proof-indent)) + +;; ((and (goto-char prevpoint) nil)) ;; just for side effect: go back to previous line +;; ;; "|" at previous line +;; ((proof-looking-at-safe coq-indent-pattern-regexp) +;; (+ prevcol proof-indent)) + +;; (t prevcol)))) + + +;; (defun coq-indent-comment-offset () +;; (save-excursion +;; (back-to-indentation) +;; (let ((oldpt (point)) +;; ;; atstart is true if the line to indent starts with a comment start +;; (atstart (proof-looking-at coq-comment-start-regexp))) +;; ;; go back looking for a non empty line +;; (if (/= (forward-line -1) 0) 0 ; we are at beginning of buffer +;; ;; only-space on a non empty line moves the point to first non space char +;; (while (and (coq-indent-only-spaces-on-line) (= (forward-line -1) 0)) ()) +;; ;; now we found the previous non empty line +;; (let ((eol (save-excursion (end-of-line) (point)))) +;; (cond +;; ;; The previous line contains is the comment start +;; ((and (not atstart) (string-match coq-comment-start-regexp +;; (buffer-substring (point) eol))) +;; (re-search-forward coq-comment-start-regexp) ;first '(*' in the line? +;; (+ 1 (current-column))) + +;; ;; the previous is in the same comment start or a comment started at that line +;; ((and (not atstart) (proof-looking-at-syntactic-context)) +;; (skip-chars-forward " \t") +;; (current-column)) + +;; ;;we were at the first line of a comment and the current line is the +;; ;;previous one +;; (t (goto-char oldpt) +;; (coq-script-parse-cmdend-backward) +;; (coq-find-real-start) +;; (current-column)))))))) + + +;; (defun coq-indent-offset (&optional notcomments) +;; (let (kind prevcol prevpoint) +;; (save-excursion +;; (setq kind (coq-back-to-indentation-prevline) ;go to previous *command* (assert) +;; prevcol (current-column) +;; prevpoint (point))) +;; ;(message "coq-indent-offset... kind = %s ; prevcol = %s; prevpoint = %s" kind prevcol prevpoint) +;; (cond +;; ((= kind 0) 0 ; top of the buffer reached +;; ) +;; ((= kind 1) ; we are at the command level +;; (+ prevcol (coq-indent-command-offset kind prevcol prevpoint))) +;; ((= kind 2) ; we are at the expression level +;; (coq-indent-expr-offset kind prevcol prevpoint nil)) +;; ((= kind 4) ; we are at the expression level inside {}s of a record +;; (coq-indent-expr-offset kind prevcol prevpoint t)) +;; ((= kind 3) +;; (if notcomments nil (coq-indent-comment-offset)))))) + +;; (defun coq-indent-calculate (&optional notcomments) +;; (coq-indent-offset notcomments)) + +;; (defun coq-indent-line () +;; "Indent current line of proof script, if indentation enabled." +;; (interactive) +;; (unless (not coq-script-indent) +;; (save-excursion +;; (let ((ind (save-excursion (back-to-indentation) (coq-indent-calculate)))) +;; (indent-line-to (max 0 ind)))) +;; (if (< (current-column) (current-indentation)) +;; (back-to-indentation)))) + +;; (defun coq-indent-line-not-comments () +;; "Same as `coq-indent-line' but comments are not indented." +;; (interactive) +;; (unless (not coq-script-indent) +;; (save-excursion +;; (let ((ind (save-excursion (back-to-indentation) (coq-indent-calculate t)))) +;; (when ind (indent-line-to (max 0 ind))))) +;; (if (< (current-column) (current-indentation)) +;; (back-to-indentation)))) + +;; (defun coq-indent-region (start end) +;; (let ((deb (min start end)) (fin (max start end))) +;; (goto-char end) +;; (setq fin (point-marker)) ;; to go back there even if shifted +;; (goto-char deb) +;; (while (< (point) fin) +;; (or (and (bolp) (eolp)) +;; (coq-indent-line-not-comments)) +;; (forward-line 1)) +;; (goto-char fin))) ;; Local Variables: *** diff --git a/coq/coq-mode.el b/coq/coq-mode.el index f5d40027..70d3952c 100644 --- a/coq/coq-mode.el +++ b/coq/coq-mode.el @@ -205,6 +205,8 @@ Near here means PT is either inside or just aside of a comment." ;; (set (make-local-variable 'adaptive-fill-function) ;; #'coq-adaptive-fill-function) + (setq-local comment-start "(*") + (setq-local comment-end "*)") (set (make-local-variable 'comment-start-skip) "(\\*+ *") (set (make-local-variable 'comment-end-skip) " *\\*+)") diff --git a/coq/coq-smie.el b/coq/coq-smie.el index 72639bc6..3d2fc3a6 100644 --- a/coq/coq-smie.el +++ b/coq/coq-smie.el @@ -41,6 +41,7 @@ ;;; Code: (require 'coq-indent) +(require 'coq-syntax) ;For coq-keywords-save-strict! (require 'smie) ; debugging @@ -351,24 +352,26 @@ The point should be at the beginning of the command name. As false positive are more annoying than false negative, return t only if it is FOR SURE a goal opener. Put a \"Proof.\" when you want to force indentation." - (save-excursion ; FIXME add other commands that potentialy open goals - (when (proof-looking-at "\\(Local\\|Global\\)?\ + (save-excursion ; FIXME add other commands that potentialy open goals + (let ((case-fold-search nil)) + (when (looking-at "\\(Local\\|Global\\)?\ \\(Definition\\|Lemma\\|Theorem\\|Fact\\|Let\\|Class\ \\|Proposition\\|Remark\\|Corollary\\|Goal\ \\|Add\\(\\s-+Parametric\\)?\\s-+Morphism\ \\|Fixpoint\\)\\>") ;; Yes Fixpoint can start a proof like Definition - (coq-lonely-:=-in-this-command)))) + (coq-lonely-:=-in-this-command))))) ;; Heuristic to detect a goal opening command: there must be a lonely ":=" (defun coq-smie-module-deambiguate () "Return t if the next command is a goal starting command. The point should be at the beginning of the command name." - (save-excursion ; FIXME Is there other module starting commands? - (cond - ((looking-back "with\\s-+" nil) "module") ; lowecase means Module that is not a declaration keyword (like in with Module) - ((proof-looking-at "\\(Module\\|Section\\)\\>") - (if (coq-lonely-:=-in-this-command) "Module start" "Module def"))))) + (save-excursion ; FIXME Is there other module starting commands? + (let ((case-fold-search nil)) + (cond + ((looking-back "with\\s-+" nil) "module") ; lowecase means Module that is not a declaration keyword (like in with Module) + ((looking-at "\\(Module\\|Section\\)\\>") + (if (coq-lonely-:=-in-this-command) "Module start" "Module def")))))) ;(defun coq-smie-detect-module-or-section-start-command () @@ -1010,12 +1013,21 @@ Typical values are 2 or 4." "Return non-nil if PARENT-POS is on same line as CHILD-POS." (= (line-number-at-pos parent-pos) (line-number-at-pos child-pos))) +(defcustom coq-indent-basic nil + "Basic indentation step. +If nil, default to `proof-indent' if it exists or to `smie-indent-basic'." + :group 'coq-mode + :type '(choice (const :tag "Fallback on global settings" nil) + integer)) + (defun coq-smie-rules (kind token) "Indentation rules for Coq. See `smie-rules-function'. KIND is the situation and TOKEN is the thing w.r.t which the rule applies." (pcase kind (`:elem (pcase token - (`basic proof-indent))) + (`basic (or coq-indent-basic + (bound-and-true-p proof-indent) + smie-indent-basic)))) (`:close-all t) (`:list-intro (or (member token '("fun" "forall" "quantif exists" "with")) 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) 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 diff --git a/generic/pg-goals.el b/generic/pg-goals.el index d9a350ec..37862a64 100644 --- a/generic/pg-goals.el +++ b/generic/pg-goals.el @@ -20,6 +20,7 @@ (eval-when-compile (require 'easymenu) ; easy-menu-add, etc (require 'span)) ; span-* +(require 'proof-script) ;For proof-insert-sendback-command (defvar proof-goals-mode-menu) ; defined by macro below (defvar proof-assistant-menu) ; defined by macro in proof-menu diff --git a/generic/pg-pbrpm.el b/generic/pg-pbrpm.el index 7a22e185..942cc919 100644 --- a/generic/pg-pbrpm.el +++ b/generic/pg-pbrpm.el @@ -38,6 +38,7 @@ (eval-when-compile (require 'proof-utils)) +(require 'proof-script) ;For proof-insert-pbp-command (require 'proof) ;;; diff --git a/generic/pg-pgip.el b/generic/pg-pgip.el index e84061b8..e7c7e344 100644 --- a/generic/pg-pgip.el +++ b/generic/pg-pgip.el @@ -38,8 +38,7 @@ (declare-function pg-response-warning "pg-response") (declare-function pg-response-message "pg-response") -(declare-function proof-segment-up-to "proof-script") -(declare-function proof-insert-pbp-command "proof-script") +(require 'proof-script) (defalias 'pg-pgip-debug 'proof-debug) (defalias 'pg-pgip-error 'error) diff --git a/generic/proof-autoloads.el b/generic/proof-autoloads.el index 4fb1f907..92c54689 100644 --- a/generic/proof-autoloads.el +++ b/generic/proof-autoloads.el @@ -17,8 +17,8 @@ (provide 'proof-autoloads) -;;;### (autoloads nil "../coq/coq" "../coq/coq.el" (23586 34852 377773 -;;;;;; 600000)) +;;;### (autoloads nil "../coq/coq" "../coq/coq.el" (23587 63448 184007 +;;;;;; 512000)) ;;; Generated autoloads from ../coq/coq.el (autoload 'coq-pg-setup "../coq/coq" "\ @@ -39,8 +39,8 @@ ;;;*** -;;;### (autoloads nil "../coq/coq-mode" "../coq/coq-mode.el" (23586 -;;;;;; 34852 373773 560000)) +;;;### (autoloads nil "../coq/coq-mode" "../coq/coq-mode.el" (23588 +;;;;;; 277 353962 216000)) ;;; Generated autoloads from ../coq/coq-mode.el (add-to-list 'auto-mode-alist '("\\.v\\'" . coq-mode)) @@ -54,8 +54,8 @@ Major mode for Coq scripts. ;;;*** -;;;### (autoloads nil "../lib/bufhist" "../lib/bufhist.el" (23586 -;;;;;; 34852 385773 680000)) +;;;### (autoloads nil "../lib/bufhist" "../lib/bufhist.el" (23587 +;;;;;; 60072 965937 641000)) ;;; Generated autoloads from ../lib/bufhist.el (autoload 'bufhist-mode "../lib/bufhist" "\ @@ -86,8 +86,8 @@ Stop keeping ring history for current buffer. ;;;*** -;;;### (autoloads nil "../lib/holes" "../lib/holes.el" (23571 60372 -;;;;;; 968579 788000)) +;;;### (autoloads nil "../lib/holes" "../lib/holes.el" (23587 60990 +;;;;;; 445008 855000)) ;;; Generated autoloads from ../lib/holes.el (autoload 'holes-set-make-active-hole "../lib/holes" "\ @@ -201,7 +201,7 @@ Insert S, expand it and replace #s and @{]s by holes. ;;;*** ;;;### (autoloads nil "../lib/maths-menu" "../lib/maths-menu.el" -;;;;;; (23577 10400 919305 444000)) +;;;;;; (23587 60072 965937 641000)) ;;; Generated autoloads from ../lib/maths-menu.el (autoload 'maths-menu-mode "../lib/maths-menu" "\ @@ -239,8 +239,8 @@ Return the list of frames displaying at least one associated buffer. ;;;*** -;;;### (autoloads nil "../lib/pg-dev" "../lib/pg-dev.el" (23577 10400 -;;;;;; 919305 444000)) +;;;### (autoloads nil "../lib/pg-dev" "../lib/pg-dev.el" (23587 60072 +;;;;;; 965937 641000)) ;;; Generated autoloads from ../lib/pg-dev.el (autoload 'profile-pg "../lib/pg-dev" "\ @@ -250,8 +250,8 @@ Configure Proof General for profiling. Use \\[elp-results] to see results. ;;;*** -;;;### (autoloads nil "pg-goals" "pg-goals.el" (23577 10400 911305 -;;;;;; 269000)) +;;;### (autoloads nil "pg-goals" "pg-goals.el" (23587 64293 950005 +;;;;;; 517000)) ;;; Generated autoloads from pg-goals.el (autoload 'proof-goals-config-done "pg-goals" "\ @@ -261,8 +261,8 @@ Initialise the goals buffer after the child has been configured. ;;;*** -;;;### (autoloads nil "pg-movie" "pg-movie.el" (23572 12305 412526 -;;;;;; 903000)) +;;;### (autoloads nil "pg-movie" "pg-movie.el" (23575 9223 344856 +;;;;;; 367000)) ;;; Generated autoloads from pg-movie.el (autoload 'pg-movie-export "pg-movie" "\ @@ -284,8 +284,8 @@ Existing XML files are overwritten. ;;;*** -;;;### (autoloads nil "pg-pamacs" "pg-pamacs.el" (23577 10400 915305 -;;;;;; 356000)) +;;;### (autoloads nil "pg-pamacs" "pg-pamacs.el" (23587 60072 961937 +;;;;;; 714000)) ;;; Generated autoloads from pg-pamacs.el (autoload 'proof-defpacustom-fn "pg-pamacs" "\ @@ -335,8 +335,8 @@ This macro also extends the `proof-assistant-settings' list. ;;;*** -;;;### (autoloads nil "pg-pgip" "pg-pgip.el" (23577 10400 915305 -;;;;;; 356000)) +;;;### (autoloads nil "pg-pgip" "pg-pgip.el" (23587 64365 208880 +;;;;;; 260000)) ;;; Generated autoloads from pg-pgip.el (autoload 'pg-pgip-process-packet "pg-pgip" "\ @@ -565,8 +565,8 @@ Parse string in ARG, same as pg-xml-parse-buffer. ;;;*** -;;;### (autoloads nil "proof-depends" "proof-depends.el" (23577 10400 -;;;;;; 915305 356000)) +;;;### (autoloads nil "proof-depends" "proof-depends.el" (23587 64458 +;;;;;; 963411 650000)) ;;; Generated autoloads from proof-depends.el (autoload 'proof-depends-process-dependencies "proof-depends" "\ @@ -608,8 +608,8 @@ Indent current line of proof script, if indentation enabled. ;;;*** -;;;### (autoloads nil "proof-maths-menu" "proof-maths-menu.el" (23577 -;;;;;; 10400 915305 356000)) +;;;### (autoloads nil "proof-maths-menu" "proof-maths-menu.el" (23587 +;;;;;; 60072 961937 714000)) ;;; Generated autoloads from proof-maths-menu.el (autoload 'proof-maths-menu-set-global "proof-maths-menu" "\ @@ -629,8 +629,8 @@ in future if we have just activated it for this buffer. ;;;*** -;;;### (autoloads nil "proof-menu" "proof-menu.el" (23586 34852 449774 -;;;;;; 323000)) +;;;### (autoloads nil "proof-menu" "proof-menu.el" (23587 60072 961937 +;;;;;; 714000)) ;;; Generated autoloads from proof-menu.el (autoload 'proof-menu-define-keys "proof-menu" "\ @@ -655,8 +655,8 @@ Construct and return PG auxiliary menu used in non-scripting buffers. ;;;*** -;;;### (autoloads nil "proof-script" "proof-script.el" (23586 34852 -;;;;;; 461774 443000)) +;;;### (autoloads nil "proof-script" "proof-script.el" (23587 64464 +;;;;;; 199330 36000)) ;;; Generated autoloads from proof-script.el (autoload 'proof-ready-for-assistant "proof-script" "\ @@ -687,24 +687,6 @@ Non-nil if the locked region is empty. Works on any buffer. \(fn)" nil nil) -(autoload 'pg-set-span-helphighlights "proof-script" "\ -Add a daughter help span for SPAN with help message, highlight, actions. -The daughter span covers the non whitespace content of the main span. - -We add the last output (when non-empty) to the hover display, and -also as the 'response property on the span. - -Optional argument MOUSEFACE means use the given face as a mouse highlight -face, if it is a face, otherwise, if it is non-nil but not a face, -do not add a mouse highlight. - -In any case, a mouse highlight and tooltip are only set if -`proof-output-tooltips' is non-nil. - -Argument FACE means add 'face property FACE to the span. - -\(fn SPAN &optional MOUSEFACE FACE)" nil nil) - (autoload 'proof-register-possibly-new-processed-file "proof-script" "\ Register a possibly new FILE as having been processed by the prover. @@ -721,21 +703,6 @@ proof assistant and Emacs has a modified buffer visiting the file. \(fn FILE &optional INFORMPROVER NOQUESTIONS)" nil nil) -(autoload 'proof-script-generic-parse-find-comment-end "proof-script" "\ -Find the end of the comment point is at the start of. Nil if not found. - -\(fn)" nil nil) - -(autoload 'proof-insert-pbp-command "proof-script" "\ -Insert CMD into the proof queue. - -\(fn CMD)" nil nil) - -(autoload 'proof-insert-sendback-command "proof-script" "\ -Insert CMD into the proof script, execute assert-until-point. - -\(fn CMD)" nil nil) - (autoload 'proof-mode "proof-script" "\ Proof General major mode class for proof scripts. \\{proof-mode-map} @@ -751,8 +718,8 @@ finish setup which depends on specific proof assistant configuration. ;;;*** -;;;### (autoloads nil "proof-shell" "proof-shell.el" (23586 34852 -;;;;;; 449774 323000)) +;;;### (autoloads nil "proof-shell" "proof-shell.el" (23587 60072 +;;;;;; 961937 714000)) ;;; Generated autoloads from proof-shell.el (autoload 'proof-shell-ready-prover "proof-shell" "\ @@ -887,8 +854,8 @@ processing. ;;;*** -;;;### (autoloads nil "proof-splash" "proof-splash.el" (23586 34852 -;;;;;; 381773 640000)) +;;;### (autoloads nil "proof-splash" "proof-splash.el" (23587 59572 +;;;;;; 767190 499000)) ;;; Generated autoloads from proof-splash.el (autoload 'proof-splash-display-screen "proof-splash" "\ @@ -906,8 +873,8 @@ Make sure the user gets welcomed one way or another. ;;;*** -;;;### (autoloads nil "proof-syntax" "proof-syntax.el" (23586 34852 -;;;;;; 453774 363000)) +;;;### (autoloads nil "proof-syntax" "proof-syntax.el" (23587 61484 +;;;;;; 723836 209000)) ;;; Generated autoloads from proof-syntax.el (autoload 'proof-replace-regexp-in-string "proof-syntax" "\ @@ -944,7 +911,7 @@ Menu made from the Proof General toolbar commands. ;;;*** ;;;### (autoloads nil "proof-unicode-tokens" "proof-unicode-tokens.el" -;;;;;; (23577 10400 919305 444000)) +;;;;;; (23587 60072 961937 714000)) ;;; Generated autoloads from proof-unicode-tokens.el (autoload 'proof-unicode-tokens-mode-if-enabled "proof-unicode-tokens" "\ @@ -971,8 +938,8 @@ is changed. ;;;*** -;;;### (autoloads nil "proof-utils" "proof-utils.el" (23586 34852 -;;;;;; 381773 640000)) +;;;### (autoloads nil "proof-utils" "proof-utils.el" (23587 60072 +;;;;;; 961937 714000)) ;;; Generated autoloads from proof-utils.el (autoload 'proof-debug "proof-utils" "\ @@ -983,8 +950,8 @@ If flag `proof-general-debug' is nil, do nothing. ;;;*** -;;;### (autoloads nil "../lib/scomint" "../lib/scomint.el" (23577 -;;;;;; 10400 919305 444000)) +;;;### (autoloads nil "../lib/scomint" "../lib/scomint.el" (23587 +;;;;;; 60072 965937 641000)) ;;; Generated autoloads from ../lib/scomint.el (autoload 'scomint-make-in-buffer "../lib/scomint" "\ @@ -1016,7 +983,7 @@ If PROGRAM is a string, the remaining SWITCHES are arguments to PROGRAM. ;;;*** ;;;### (autoloads nil "../lib/texi-docstring-magic" "../lib/texi-docstring-magic.el" -;;;;;; (23577 10400 919305 444000)) +;;;;;; (23587 60072 965937 641000)) ;;; Generated autoloads from ../lib/texi-docstring-magic.el (autoload 'texi-docstring-magic "../lib/texi-docstring-magic" "\ @@ -1042,7 +1009,7 @@ in your Emacs font. ;;;*** ;;;### (autoloads nil "../lib/unicode-tokens" "../lib/unicode-tokens.el" -;;;;;; (23577 10400 923305 531000)) +;;;;;; (23587 60072 965937 641000)) ;;; Generated autoloads from ../lib/unicode-tokens.el (autoload 'unicode-tokens-encode-str "../lib/unicode-tokens" "\ @@ -1060,8 +1027,8 @@ Return a unicode encoded version presentation of STR. ;;;;;; "../lib/pg-fontsets.el" "../lib/proof-compat.el" "../lib/span.el" ;;;;;; "pg-autotest.el" "pg-custom.el" "pg-pbrpm.el" "pg-vars.el" ;;;;;; "proof-auxmodes.el" "proof-config.el" "proof-faces.el" "proof-site.el" -;;;;;; "proof-tree.el" "proof-useropts.el" "proof.el") (23586 34852 -;;;;;; 457774 403000)) +;;;;;; "proof-tree.el" "proof-useropts.el" "proof.el") (23588 1830 +;;;;;; 459568 860000)) ;;;*** diff --git a/generic/proof-depends.el b/generic/proof-depends.el index 372ce06b..163a0968 100644 --- a/generic/proof-depends.el +++ b/generic/proof-depends.el @@ -26,6 +26,7 @@ (require 'cl-lib) (require 'span) (require 'pg-vars) +(require 'proof-script) ;For pg-set-span-helphighlights (require 'proof-config) (require 'proof-autoloads) 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 diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el index 777d3858..cdc38775 100644 --- a/generic/proof-syntax.el +++ b/generic/proof-syntax.el @@ -25,9 +25,9 @@ (defsubst proof-ids-to-regexp (l) "Maps a non-empty list of tokens L to a regexp matching any element. Uses a regexp of the form \\_<...\\_>." - (concat "\\_<\\(?:" + (concat "\\_<" (regexp-opt l) ; was: (mapconcat 'identity l "\\|") - "\\)\\_>")) + "\\_>")) (defsubst proof-anchor-regexp (e) "Anchor (\\`) and group the regexp E." 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) -- cgit v1.2.3