diff options
| author |  Stefan Monnier <monnier@iro.umontreal.ca> | 2018-12-26 18:00:43 -0500 |
|---|---|---|
| committer | Stefan Monnier <monnier@iro.umontreal.ca> | 2018-12-26 18:00:43 -0500 |
| commit | fb3b75dab55b6e6befffc53e136422558be5faa0 (patch) | |
| tree | b3ec11dfb4581ec752057b98c638ee00a6c59f41 | |
| parent | 7389d43893569ff0e1eff892254901876fc8225e (diff) | |
Make coq-mode work without generic/proof-*
Revise the various `require`s to avoid spurious dependencies, and tweak
the code here and there to eliminate the remaining dependencies.
* coq/coq-db.el: Don't require proof-config nor proof-syntax.
(coq-build-opt-regexp-from-db): Avoid proof-regexp-alt-list.
* coq/coq-indent.el: Use lexical-binding. Don't require coq-syntax.
Comment out all the code that's not used any more.
(coq-empty-command-p): Use forward-comment instead of
coq-find-not-in-comment-backward. Fix paren typos.
(coq-script-parse-cmdend-forward, coq-script-parse-cmdend-backward):
Use forward-comment i.s.o proof-script-generic-parse-find-comment-end.
Use syntax-ppss i.s.o proof-buffer-syntactic-context.
(coq-find-current-start): Explicit case-fold-search i.s.o proof-looking-at.
* coq/coq-mode.el (coq-mode): Set comment-start/end.
* coq/coq-smie.el: Require coq-syntax explicitly.
(coq-smie-detect-goal-command, coq-smie-module-deambiguate):
Explicit case-fold-search i.s.o proof-looking-at.
(coq-indent-basic): New custom var.
(coq-smie-rules): Use it in case PG is not loaded.
* coq/coq-syntax.el: Don't require proof-syntax, proof-utils, and span.
(coq-goal-command-p): Use overlay-get i.s.o span-property.
(coq-save-command-regexp-strict, coq-save-command-regexp):
Use \` and regexp-opt i.s.o proof-anchor-regexp and proof-ids-to-regexp.
(coq-save-command-p): Explicit case-fold-search i.s.o proof-string-match.
(coq--regexp-alt-list-symb): Rename from proof-regexp-alt-list-symb.
Use mapconcat i.s.o proof-regexp-alt-list.
(coq-save-with-hole-regexp): Use regexp-opt i.s.o proof-regexp-alt-list.
(coq-goal-command-regexp, coq-goal-with-hole-regexp)
(coq-decl-with-hole-regexp, coq-defn-with-hole-regexp)
(coq-font-lock-keywords-1): Use mapconcat i.s.o proof-regexp-alt-list.
(coq-find-first-hyp, coq-detect-hyps-positions-in-goals):
Use current buffer i.s.o proof-goals-buffer.
(coq-with-altered-syntax-table): Fix broken use of unwind-protect.
* coq/coq.el (coq-detect-hyps-in-goals): Change buffer before calling
coq-find-first-hyp and coq-detect-hyps-positions-in-goals.
(coq-pg-setup): Use comment-start/end.
* generic/pg-goals.el: Require proof-script explicitly instead of
autoloading via proof-insert-sendback-command.
* generic/pg-pbrpm.el: Require proof-script explicitly instead of
autoloading via proof-insert-pbp-command.
* generic/pg-pgip.el: Require proof-script explicitly.
* generic/proof-depends.el: Require proof-script explicitly instead of
autoloading via pg-set-span-helphighlights.
* generic/proof-script.el (pg-set-span-helphighlights)
(proof-insert-pbp-command, proof-insert-sendback-command)
(proof-script-generic-parse-find-comment-end): Don't autoload.
* generic/proof-syntax.el (proof-ids-to-regexp): Simplify.
* lib/span.el (span-delete): η-reduce.
| -rw-r--r-- | coq/coq-db.el | 4 | ||||
| -rw-r--r-- | coq/coq-indent.el | 1547 | ||||
| -rw-r--r-- | coq/coq-mode.el | 2 | ||||
| -rw-r--r-- | coq/coq-smie.el | 30 | ||||
| -rw-r--r-- | coq/coq-syntax.el | 85 | ||||
| -rw-r--r-- | coq/coq.el | 12 | ||||
| -rw-r--r-- | generic/pg-goals.el | 1 | ||||
| -rw-r--r-- | generic/pg-pbrpm.el | 1 | ||||
| -rw-r--r-- | generic/pg-pgip.el | 3 | ||||
| -rw-r--r-- | generic/proof-autoloads.el | 117 | ||||
| -rw-r--r-- | generic/proof-depends.el | 1 | ||||
| -rw-r--r-- | generic/proof-script.el | 4 | ||||
| -rw-r--r-- | generic/proof-syntax.el | 4 | ||||
| -rw-r--r-- | 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 "\\_<match\\_>" str)) - (with (coq-count-match "\\_<with\\_>" str)) - (letwith (+ (coq-count-match "\\_<let\\_>" 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 "\\_<match\\_>" str)) +;; (with (coq-count-match "\\_<with\\_>" str)) +;; (letwith (+ (coq-count-match "\\_<let\\_>" 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 "\\<Tim") (- (point) 3)) - (and (looking-at "l\\>") (looking-back "\\<Fai") (- (point) 3)) - (and (looking-at "\"") (looking-back "\\<Redirect\\s-+\"[^\"]+")) - (and (looking-at "[[:digit:]]\\_>") (looking-back "\\<Timeout\\s-+[[:digit:]]*"))) - (goto-char (match-beginning 0)) - (coq-empty-command-p)) - ;; not a bullet, we found something else, it should be either a - ;; dot or the beginning of the file, otherwise we are in the - ;; middle of a command - (t (looking-at "\\.\\|\\`")) - ))) + (forward-comment (- (point))) + (unless (bobp) (forward-char -1)) + ;; 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 "\\<Tim" (- (point) 3))) + (and (looking-at "l\\>") (looking-back "\\<Fai" (- (point) 3))) + (and (looking-at "\"") (looking-back "\\<Redirect\\s-+\"[^\"]+")) + (and (looking-at "[[:digit:]]\\_>") (looking-back "\\<Timeout\\s-+[[:digit:]]*"))) + (goto-char (match-beginning 0)) + (coq-empty-command-p)) + ;; not a bullet, we found something else, it should be either a + ;; dot or the beginning of the file, otherwise we are in the + ;; middle of a command + (t (looking-at "\\.\\|\\`")) + )) ; slight modification of proof-script-generic-parse-cmdend (one of the @@ -414,9 +413,9 @@ substring if present). If no end command is found, go as far as possible and return nil. End of command appearing in comments are ignored. This function makes use of the substring 1 of the command end regexp." - (if (looking-at proof-script-comment-start-regexp) + (if (looking-at comment-start-skip) ;; Handle comments - (if (proof-script-generic-parse-find-comment-end) 'comment) + (if (forward-comment 1) 'comment) ;; Handle non-comments: assumed to be commands (if (< (coq-is-on-ending-context) 0) (ignore-errors (forward-char (coq-is-on-ending-context)))) @@ -443,7 +442,7 @@ regexp." (not (coq-empty-command-p)))) (and (goto-char foundend) - (proof-buffer-syntactic-context)))) + (nth 8 (syntax-ppss))))) ;; Given the form of coq-end-command-regexp ;; match-end 1 is the right place to start again ;; to search backward, next time we start from just @@ -451,7 +450,7 @@ regexp." (ignore-errors (goto-char foundend))) (if (and foundend (goto-char foundend) ; 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 @@ -467,9 +466,9 @@ regexp." Point is put exactly before the last ending token (before the last \".\" if \"...\"). If no end command is found, go as far as possible and return nil." - (if (looking-at proof-script-comment-start-regexp) + (if (looking-at comment-start-skip) ;; Handle comments - (if (proof-script-generic-parse-find-comment-end) 'comment) ; start? + (if (forward-comment 1) 'comment) ; start? ;; Handle non-comments: assumed to be commands ;; first shift if we are in the middle of a ending pattern (if (> (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 "\\<Proof\\>") 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 "\\<Proof\\>") 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 "\\<then\\>") - (save-excursion - (coq-find-unclosed 1 real-start "\\<if\\>" "\\<then\\>") - (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 "\\<else\\>") - (save-excursion - (coq-find-unclosed 1 real-start "\\<then\\>" "\\<else\\>") - (coq-find-unclosed 1 real-start "\\<if\\>" "\\<then\\>") - (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 "\\<then\\>") +;; (save-excursion +;; (coq-find-unclosed 1 real-start "\\<if\\>" "\\<then\\>") +;; (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 "\\<else\\>") +;; (save-excursion +;; (coq-find-unclosed 1 real-start "\\<then\\>" "\\<else\\>") +;; (coq-find-unclosed 1 real-start "\\<if\\>" "\\<then\\>") +;; (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-*\\(\\.\\|\\_<with\\_>\\|\\_<using\\_>\\)" 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-*\\(\\.\\|\\_<with\\_>\\|\\_<using\\_>\\)" 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) @@ -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) |