diff options
Diffstat (limited to 'coq')
| -rw-r--r-- | coq/coq-abbrev.el | 48 | ||||
| -rw-r--r-- | coq/coq-indent.el | 2 | ||||
| -rw-r--r-- | coq/coq-smie.el | 319 | ||||
| -rw-r--r-- | coq/coq-syntax.el | 64 | ||||
| -rw-r--r-- | coq/coq.el | 119 |
5 files changed, 252 insertions, 300 deletions
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index 308ca865..a15db325 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -1,9 +1,9 @@ -;;; coq-abbrev.el --- coq abbrev table and menus for ProofGeneral mode +;;; coq-abbrev.el --- coq abbrev table and menus for ProofGeneral mode -*- lexical-binding:t -*- ;; This file is part of Proof General. ;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh -;; Portions © Copyright 2003, 2012, 2014 Free Software Foundation, Inc. +;; Portions © Copyright 2003-2018 Free Software Foundation, Inc. ;; Portions © Copyright 2001-2017 Pierre Courtieu ;; Portions © Copyright 2010, 2016 Erik Martin-Dorel ;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews @@ -68,46 +68,10 @@ ;;; The abbrev table built from keywords tables ;#s and @{..} are replaced by holes by holes-abbrev-complete -(defun coq-install-abbrevs () - "Install default abbrev table for coq if no other already is." - (if (boundp 'coq-mode-abbrev-table) - ;; da: this test will always fail. Assume bound-->non-empty - ;; (not (equal coq-mode-abbrev-table (make-abbrev-table)))) - (message "Coq abbrevs already exists, default not loaded") - (define-abbrev-table 'coq-mode-abbrev-table - (append coq-tactics-abbrev-table coq-tacticals-abbrev-table - coq-commands-abbrev-table coq-terms-abbrev-table)) - ;; if we use default coq abbrev, never ask to save it - ;; PC: fix trac #382 I comment this. But how to disable abbrev - ;; saving for coq mode only? - ;;(setq save-abbrevs nil) ; - ;; DA: how about above, just temporarily disable saving? - (message "Coq default abbrevs loaded"))) - -(unless (or noninteractive (bound-and-true-p byte-compile-current-file)) - (coq-install-abbrevs)) -;;;;; - -; Redefining this macro to change the way a string option is asked to -; the user: we pre fill the answer with current value of the option; -(defun proof-defstringset-fn (var &optional othername) - "Define a function <VAR>-toggle for setting an integer customize setting VAR. -Args as for the macro `proof-defstringset', except will be evaluated." - (eval - `(defun ,(if othername othername - (intern (concat (symbol-name var) "-stringset"))) (arg) - ,(concat "Set `" (symbol-name var) "' to ARG. -This function simply uses customize-set-variable to set the variable. -It was constructed with `proof-defstringset-fn'.") -; (interactive ,(format "sValue for %s (a string, currenly %s): " -; (symbol-name var) (symbol-value var))) - (interactive (list - (read-string - (format "Value for %s (float): " - (symbol-name (quote ,var)) - (symbol-value (quote ,var))) - (symbol-value (quote ,var))))) - (customize-set-variable (quote ,var) arg)))) +(define-abbrev-table 'coq-mode-abbrev-table + (append coq-tactics-abbrev-table coq-tacticals-abbrev-table + coq-commands-abbrev-table coq-terms-abbrev-table) + "Abbrev table for Coq.") ;; The coq menu partly built from tables diff --git a/coq/coq-indent.el b/coq/coq-indent.el index af780251..ba4db8c3 100644 --- a/coq/coq-indent.el +++ b/coq/coq-indent.el @@ -523,7 +523,7 @@ the (point-min) if there is no previous command." "Move to the start of command at point. The point is put exactly before first non comment letter of the command." (coq-find-current-start) - (coq-find-not-in-comment-forward "\\S-")) + (forward-comment (point-max))) (defun same-line (pt pt2) (or (= (line-number-at-pos pt) (line-number-at-pos pt2)))) diff --git a/coq/coq-smie.el b/coq/coq-smie.el index 15697354..72639bc6 100644 --- a/coq/coq-smie.el +++ b/coq/coq-smie.el @@ -1,9 +1,9 @@ -;;; coq-smie.el --- SMIE lexer, grammar, and indent rules for Coq +;;; coq-smie.el --- SMIE lexer, grammar, and indent rules for Coq -*- lexical-binding:t -*- ;; This file is part of Proof General. ;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh -;; Portions © Copyright 2003, 2012, 2014 Free Software Foundation, Inc. +;; Portions © Copyright 2003-2018 Free Software Foundation, Inc. ;; Portions © Copyright 2001-2017 Pierre Courtieu ;; Portions © Copyright 2010, 2016 Erik Martin-Dorel ;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews @@ -41,7 +41,7 @@ ;;; Code: (require 'coq-indent) -(require 'smie nil 'noerror) +(require 'smie) ; debugging ;(defmacro measure-time (&rest body) @@ -64,21 +64,22 @@ indentation work well." :group 'coq) -(defun coq-string-suffix-p (str1 str2 &optional ignore-case) +(defalias 'coq--string-suffix-p + ;; Replacement for emacs < 24.4, borrowed from sindikat at + ;; stackoverflow efficient if bytecompiled, builtin version is + ;; probably better when it exists + (if (fboundp 'string-suffix-p) + 'string-suffix-p + (lambda (str1 str2 &optional ignore-case) "Return non-nil if STR1 is a prefix of STR2. If IGNORE-CASE is non-nil, the comparison is done without paying attention to case differences." (let ((begin2 (- (length str2) (length str1))) (end2 (length str2))) (when (< begin2 0) (setq begin2 0)) ; to avoid negative begin2 - (eq t (compare-strings str1 nil nil str2 begin2 end2 ignore-case)))) + (eq t (compare-strings str1 nil nil str2 begin2 end2 ignore-case)))))) + -;; Replacement for emacs < 24.4, borrowed from sindikat at -;; stackoverflow efficient if bytecompiled, builtin version is -;; probably better when it exists -(unless (fboundp 'string-suffix-p) - (fset 'string-suffix-p 'coq-string-suffix-p) - (declare-function string-suffix-p "smie")) ;; As any user defined notation ending with "." will break ;; proofgeneral synchronization anyway, let us consider that any @@ -145,12 +146,13 @@ intros. or Proof foo. the token of \".\" is simply \".\"." (save-excursion - (let ((p (point)) (beg (coq-find-real-start))) ; moves to real start of command + (let ((p (point))) + (coq-find-real-start) ; Move to real start of command. (cond ((looking-at "BeginSubproof\\>") ". proofstart") ((looking-at "Proof\\>") (forward-char 5) - (coq-find-not-in-comment-forward "[^[:space:]]") ;; skip spaces and comments + (forward-comment (point-max)) (if (looking-at "\\.\\|with\\|using") ". proofstart" ".")) ((or (looking-at "Next\\s-+Obligation\\>") (coq-smie-detect-goal-command)) @@ -211,26 +213,28 @@ the token of \".\" is simply \".\"." (defun coq-backward-token-fast-nogluing-dot-friends () (forward-comment (- (point))) - (let ((pt (point))) - (let* ((tok-punc (skip-syntax-backward ".")) - (str-punc (buffer-substring-no-properties pt (point))) - (tok-other (if (zerop tok-punc) (skip-syntax-backward "w_'")))) - ;; special case: if the symbols found end by "." or ";", then consider this last letter alone as a token - (when (and (not (zerop tok-punc)) (string-match "\\s.+[.;]" str-punc)) - (skip-syntax-forward ".") - (forward-char -1)) - (buffer-substring-no-properties pt (point))))) + (let* ((pt (point)) + (tok-punc (skip-syntax-backward ".")) + (str-punc (buffer-substring-no-properties pt (point)))) + (if (zerop tok-punc) (skip-syntax-backward "w_'")) + ;; Special case: if the symbols found end by "." or ";", + ;; then consider this last letter alone as a token + (when (and (not (zerop tok-punc)) (string-match "\\s.+[.;]" str-punc)) + (skip-syntax-forward ".") + (forward-char -1)) + (buffer-substring-no-properties pt (point)))) (defun coq-forward-token-fast-nogluing-dot-friends () (forward-comment (point-max)) - (let ((pt (point))) - (let* ((tok-punc (skip-syntax-forward ".")) - (str-punc (buffer-substring-no-properties pt (point))) - (tok-other (if (zerop tok-punc) (skip-syntax-forward "w_'")))) - ;; special case: if the symbols found end by "." or ";", then consider this last letter alone as a token - (when (and (not (zerop tok-punc)) (string-match "\\s.+[.;]" str-punc)) - (forward-char -1)) - (buffer-substring-no-properties pt (point))))) + (let* ((pt (point)) + (tok-punc (skip-syntax-forward ".")) + (str-punc (buffer-substring-no-properties pt (point)))) + (if (zerop tok-punc) (skip-syntax-forward "w_'")) + ;; Special case: if the symbols found end by "." or ";", + ;; then consider this last letter alone as a token + (when (and (not (zerop tok-punc)) (string-match "\\s.+[.;]" str-punc)) + (forward-char -1)) + (buffer-substring-no-properties pt (point)))) ;; ignore-between is a description of pseudo delimiters of blocks that ;; should be jumped when searching. There is a bad interaction when @@ -298,8 +302,7 @@ inside parenthesis)." ; if we find something to ignore, we directly jump to the ; corresponding openner (if parop - (let ((p (point)) - (parops ; corresponding matcher may be a list + (let ((parops ; corresponding matcher may be a list (if (listp (car parop)) (car parop) (cons (car parop) nil)))) ; go to corresponding closer or meet "." ;(message "newpatterns = %S" (append parops (cons "." nil))) @@ -386,9 +389,9 @@ The point should be at the beginning of the command name." (equal (point) (save-excursion (coq-find-real-start)))) -(defun coq-is-bullet-token (tok) (string-suffix-p "bullet" tok)) -(defun coq-is-subproof-token (tok) (string-suffix-p "subproof" tok)) -(defun coq-is-dot-token (tok) (or (string-suffix-p "proofstart" tok) +(defun coq-is-bullet-token (tok) (coq--string-suffix-p "bullet" tok)) +(defun coq-is-subproof-token (tok) (coq--string-suffix-p "subproof" tok)) +(defun coq-is-dot-token (tok) (or (coq--string-suffix-p "proofstart" tok) (string-equal "." tok))) (defun coq-is-cmdend-token (tok) (or (coq-is-bullet-token tok) (coq-is-subproof-token tok) (coq-is-dot-token tok))) @@ -509,7 +512,7 @@ The point should be at the beginning of the command name." ((member corresp '("Inductive" "CoInductive" "Variant")) ":= inductive") ((equal corresp "let") ":= let") ((equal corresp "where") ":= inductive") ;; inductive or fixpoint, nevermind - ((or (looking-back "{" nil)) ":= record") + ((or (eq ?\{ (char-before))) ":= record") (t ":=")))) ; a parenthesis stopped the search @@ -541,8 +544,8 @@ The point should be at the beginning of the command name." (cond ((member backtok '("." "Ltac")) "; tactic") ((equal backtok nil) - (if (or (looking-back "(" nil) (looking-back "\\[") - (and (looking-back "{" nil) + (if (or (memq (char-before) '(?\( ?\[)) + (and (eq (char-before) ?\{) (equal (coq-smie-backward-token) "{ subproof"))) ;; recursive call "; tactic" "; record")))))) @@ -558,10 +561,10 @@ The point should be at the beginning of the command name." (equal (coq-smie-backward-token) "; tactic")) ;; recursive "|| tactic") ;; this is wrong half of the time but should not harm indentation - ((and (equal backtok nil) (looking-back "(" nil)) "||") + ((and (equal backtok nil) (eq (char-before) '?\()) "||") ((equal backtok nil) - (if (or (looking-back "\\[" nil) - (and (looking-back "{" nil) + (if (or (eq (char-before) '?\[) + (and (eq (char-before) '?\{) (equal (coq-smie-backward-token) "{ subproof"))) ;; recursive call "|| tactic" "||")))))) @@ -618,7 +621,8 @@ The point should be at the beginning of the command name." ;; (forward-char -1) ;; (if (looking-at "{") "{ subproof" "} subproof")) - ((and (equal tok ":") (looking-back "\\<\\(constr\\|ltac\\|uconstr\\)" nil)) + ((and (equal tok ":") (looking-back "\\<\\(constr\\|ltac\\|uconstr\\)" + (- (point) 7))) ": ltacconstr") ((member tok '(":=" "::=")) @@ -848,113 +852,112 @@ Typical values are 2 or 4." ;; greatly simplify this file. We should ask Stefan Monnier how to ;; have two grammars with smie. (defconst coq-smie-grammar - (when (fboundp 'smie-prec2->grammar) - (smie-prec2->grammar - (smie-bnf->prec2 - '((exp - (exp ":= def" exp) - (exp ":=" exp) (exp ":= inductive" exp) - (exp "||" exp) (exp "|" exp) (exp "=>" exp) - (exp "xxx provedby" exp) (exp "as morphism" exp) - (exp "with signature" exp) - ("match" matchexp "with match" exp "end");expssss - ("let" assigns "in let" exp) ;("eval in" assigns "in eval" exp) disabled - ("fun" exp "=> fun" exp) ("if" exp "then" exp "else" exp) - ("quantif exists" exp ", quantif" exp) - ("forall" exp ", quantif" exp) - ;;; - ("(" exp ")") ("{|" exps "|}") ("{" exps "}") - (exp "; tactic" exp) (exp "in tactic" exp) (exp "as" exp) - (exp "by" exp) (exp "with" exp) (exp "|-" exp) - (exp ":" exp) (exp ":<" exp) (exp "," exp) - (exp "->" exp) (exp "<->" exp) (exp "&" exp) - (exp "/\\" exp) (exp "\\/" exp) - (exp "==" exp) (exp "=" exp) (exp "<>" exp) (exp "<=" exp) - (exp "<" exp) (exp ">=" exp) (exp ">" exp) - (exp "=?" exp) (exp "<=?" exp) (exp "<?" exp) - (exp "^" exp) - (exp "+" exp) (exp "-" exp) - (exp "*" exp) - (exp ": ltacconstr" exp)(exp ". selector" exp)) - ;; Having "return" here rather than as a separate rule in `exp' causes - ;; it to be indented at a different level than "with". - (matchexp (exp) (exp "as match" exp) (exp "in match" exp) - (exp "return" exp) ) - (exps (affectrec) (exps "; record" exps)) - (affectrec (exp ":= record" exp)) - (assigns (exp ":= let" exp)) ;(assigns "; record" assigns) - - (moduledef (moduledecl ":= module" exp)) - (moduledecl (exp) (exp ":" moduleconstraint) - (exp "<:" moduleconstraint)) - (moduleconstraint - (exp) (exp ":= with" exp) - (moduleconstraint "with module" "module" moduleconstraint)) - - ;; To deal with indentation inside module declaration and inside - ;; proofs, we rely on the lexer. The lexer detects "." terminator of - ;; goal starter and returns the ". proofstart" and ". moduelstart" - ;; tokens. - (bloc ("{ subproof" commands "} subproof") - (". proofstart" commands "Proof End") - (". modulestart" commands "end module" exp) - (moduledecl) (moduledef) - (exp)) - - (commands (commands "." commands) - (commands "- bullet" commands) - (commands "+ bullet" commands) - (commands "* bullet" commands) - (commands "-- bullet" commands) - (commands "++ bullet" commands) - (commands "** bullet" commands) - (commands "--- bullet" commands) - (commands "+++ bullet" commands) - (commands "*** bullet" commands) - (commands "---- bullet" commands) - (commands "++++ bullet" commands) - (commands "**** bullet" commands) - ;; "with" of mutual definition should act like "." - ;; same for "where" (introduction of a notation - ;; after a inductive or fixpoint) - (commands "with inductive" commands) - (commands "with fixpoint" commands) - (commands "where" commands) - (bloc))) - - - ;; Resolve the "trailing expression ambiguity" as in "else x -> b". - ;; each line orders tokens by increasing priority - ;; | C x => fun a => b | C2 x => ... - ;;'((assoc "=>") (assoc "|") (assoc "|-" "=> fun")) ; (assoc ", quantif") - '((assoc "- bullet") (assoc "+ bullet") (assoc "* bullet") - (assoc "-- bullet") (assoc "++ bullet") (assoc "** bullet") - (assoc "--- bullet") (assoc "+++ bullet") (assoc "*** bullet") - (assoc "---- bullet") (assoc "++++ bullet") (assoc "**** bullet") - (assoc ".") - (assoc "with inductive" "with fixpoint" "where")) - '((assoc ":= def" ":= inductive") - (assoc "|") (assoc "=>") - (assoc ":=") (assoc "xxx provedby") - (assoc "as morphism") (assoc "with signature") (assoc "with match") - (assoc "in let") - (assoc "in eval") (assoc "=> fun") (assoc "then") (assoc ", quantif") - (assoc "|| tactic") ;; FIXME: detecting "+ tactic" and "|| tactic" seems impossible - (assoc "; tactic") (assoc "in tactic") (assoc "as" "by") (assoc "with") - (assoc "|-") (assoc ":" ":<") (assoc ",") - (assoc "else") - (assoc "->") (assoc "<->") - (assoc "&") (assoc "/\\") (assoc "\\/") - (assoc "==") (assoc "=") (assoc "<" ">" "<=" ">=" "<>") - (assoc "=?") (assoc "<=?") (assoc "<?") (assoc "^") - (assoc "||") ;; FIXME: detecting "+ tactic" and "|| tactic" seems impossible - (assoc "+") (assoc "-") (assoc "*") - (assoc ": ltacconstr") (assoc ". selector")) - '((assoc ":" ":<") (assoc "<")) - '((assoc ". modulestart" "." ". proofstart") (assoc "Module def") - (assoc "with module" "module") (assoc ":= module") - (assoc ":= with") (assoc ":" ":<")) - '((assoc ":= def") (assoc "; record") (assoc ":= record"))))) + (smie-prec2->grammar + (smie-bnf->prec2 + '((exp + (exp ":= def" exp) + (exp ":=" exp) (exp ":= inductive" exp) + (exp "||" exp) (exp "|" exp) (exp "=>" exp) + (exp "xxx provedby" exp) (exp "as morphism" exp) + (exp "with signature" exp) + ("match" matchexp "with match" exp "end") ;expssss + ("let" assigns "in let" exp) ;("eval in" assigns "in eval" exp) disabled + ("fun" exp "=> fun" exp) ("if" exp "then" exp "else" exp) + ("quantif exists" exp ", quantif" exp) + ("forall" exp ", quantif" exp) +;;; + ("(" exp ")") ("{|" exps "|}") ("{" exps "}") + (exp "; tactic" exp) (exp "in tactic" exp) (exp "as" exp) + (exp "by" exp) (exp "with" exp) (exp "|-" exp) + (exp ":" exp) (exp ":<" exp) (exp "," exp) + (exp "->" exp) (exp "<->" exp) (exp "&" exp) + (exp "/\\" exp) (exp "\\/" exp) + (exp "==" exp) (exp "=" exp) (exp "<>" exp) (exp "<=" exp) + (exp "<" exp) (exp ">=" exp) (exp ">" exp) + (exp "=?" exp) (exp "<=?" exp) (exp "<?" exp) + (exp "^" exp) + (exp "+" exp) (exp "-" exp) + (exp "*" exp) + (exp ": ltacconstr" exp)(exp ". selector" exp)) + ;; Having "return" here rather than as a separate rule in `exp' causes + ;; it to be indented at a different level than "with". + (matchexp (exp) (exp "as match" exp) (exp "in match" exp) + (exp "return" exp) ) + (exps (affectrec) (exps "; record" exps)) + (affectrec (exp ":= record" exp)) + (assigns (exp ":= let" exp)) ;(assigns "; record" assigns) + + (moduledef (moduledecl ":= module" exp)) + (moduledecl (exp) (exp ":" moduleconstraint) + (exp "<:" moduleconstraint)) + (moduleconstraint + (exp) (exp ":= with" exp) + (moduleconstraint "with module" "module" moduleconstraint)) + + ;; To deal with indentation inside module declaration and inside + ;; proofs, we rely on the lexer. The lexer detects "." terminator of + ;; goal starter and returns the ". proofstart" and ". moduelstart" + ;; tokens. + (bloc ("{ subproof" commands "} subproof") + (". proofstart" commands "Proof End") + (". modulestart" commands "end module" exp) + (moduledecl) (moduledef) + (exp)) + + (commands (commands "." commands) + (commands "- bullet" commands) + (commands "+ bullet" commands) + (commands "* bullet" commands) + (commands "-- bullet" commands) + (commands "++ bullet" commands) + (commands "** bullet" commands) + (commands "--- bullet" commands) + (commands "+++ bullet" commands) + (commands "*** bullet" commands) + (commands "---- bullet" commands) + (commands "++++ bullet" commands) + (commands "**** bullet" commands) + ;; "with" of mutual definition should act like "." + ;; same for "where" (introduction of a notation + ;; after a inductive or fixpoint) + (commands "with inductive" commands) + (commands "with fixpoint" commands) + (commands "where" commands) + (bloc))) + + + ;; Resolve the "trailing expression ambiguity" as in "else x -> b". + ;; each line orders tokens by increasing priority + ;; | C x => fun a => b | C2 x => ... + ;;'((assoc "=>") (assoc "|") (assoc "|-" "=> fun")) ; (assoc ", quantif") + '((assoc "- bullet") (assoc "+ bullet") (assoc "* bullet") + (assoc "-- bullet") (assoc "++ bullet") (assoc "** bullet") + (assoc "--- bullet") (assoc "+++ bullet") (assoc "*** bullet") + (assoc "---- bullet") (assoc "++++ bullet") (assoc "**** bullet") + (assoc ".") + (assoc "with inductive" "with fixpoint" "where")) + '((assoc ":= def" ":= inductive") + (assoc "|") (assoc "=>") + (assoc ":=") (assoc "xxx provedby") + (assoc "as morphism") (assoc "with signature") (assoc "with match") + (assoc "in let") + (assoc "in eval") (assoc "=> fun") (assoc "then") (assoc ", quantif") + (assoc "|| tactic") ;; FIXME: detecting "+ tactic" and "|| tactic" seems impossible + (assoc "; tactic") (assoc "in tactic") (assoc "as" "by") (assoc "with") + (assoc "|-") (assoc ":" ":<") (assoc ",") + (assoc "else") + (assoc "->") (assoc "<->") + (assoc "&") (assoc "/\\") (assoc "\\/") + (assoc "==") (assoc "=") (assoc "<" ">" "<=" ">=" "<>") + (assoc "=?") (assoc "<=?") (assoc "<?") (assoc "^") + (assoc "||") ;; FIXME: detecting "+ tactic" and "|| tactic" seems impossible + (assoc "+") (assoc "-") (assoc "*") + (assoc ": ltacconstr") (assoc ". selector")) + '((assoc ":" ":<") (assoc "<")) + '((assoc ". modulestart" "." ". proofstart") (assoc "Module def") + (assoc "with module" "module") (assoc ":= module") + (assoc ":= with") (assoc ":" ":<")) + '((assoc ":= def") (assoc "; record") (assoc ":= record")))) "Parsing table for Coq. See `smie-grammar'.") ;; FIXME: ; Record rec:Set := { @@ -1010,11 +1013,11 @@ Typical values are 2 or 4." (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." - (case kind - (:elem (case token - (basic proof-indent))) - (:close-all t) - (:list-intro + (pcase kind + (`:elem (pcase token + (`basic proof-indent))) + (`:close-all t) + (`:list-intro (or (member token '("fun" "forall" "quantif exists" "with")) ;; We include "." in list-intro for the ". { .. } \n { .. }" so the ;; second {..} is aligned with the first rather than being indented as @@ -1026,7 +1029,7 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies." ; (forward-char 1) ; skip de "." ; (equal (coq-smie-forward-token) "{ subproof")) )) - (:after + (`:after (cond ;; Override the default indent step added because of their presence ;; in smie-closer-alist. @@ -1064,7 +1067,9 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies." (not (coq-smie-is-ltacdef)) (not (coq-smie-is-inside-parenthesized-tactic)) (or (not (smie-rule-parent-p "; tactic")) - (and smie--parent + ;; FIXME: Don't depend on SMIE's internals! + (and (boundp 'smie--parent) + smie--parent (coq-smie--same-line-as-parent (nth 1 smie--parent) (point))))) coq-indent-semicolon-tactical @@ -1089,7 +1094,7 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies." (save-excursion (forward-char -1) (coq-find-real-start) `(column . ,(+ coq-indent-modulestart (current-column))))))) - (:before + (`:before (cond ; ((and (member token '("{ subproof")) diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index e1a9a7e3..7a11a43f 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -1,4 +1,4 @@ -;;; coq-syntax.el --- Font lock expressions for Coq +;;; coq-syntax.el --- Font lock expressions for Coq -*- lexical-binding:t -*- ;; This file is part of Proof General. @@ -987,14 +987,15 @@ so for the following reasons: ;; elle declare un module. ;; (la fonction vernac_declare_module dans toplevel/vernacentries) -(defun coq-count-match (regexp strg) - "Count the number of max. non-overlapping substring of STRG matching REGEXP. +(defun coq-count-match (regexp str) + "Count the number of max. non-overlapping substring of STR matching REGEXP. Empty matches are counted once." - (let ((nbmatch 0) (str strg)) - (while (and (proof-string-match regexp str) (not (string-equal str ""))) + (let ((nbmatch 0) (pos 0) (end (length str)) + (case-fold-search nil)) + (while (and (< pos end) + (string-match regexp str pos)) (cl-incf nbmatch) - (if (= (match-end 0) 0) (setq str (substring str 1)) - (setq str (substring str (match-end 0))))) + (setq pos (max (match-end 0) (1+ pos)))) nbmatch)) ;; Module and or section openings are detected syntactically. Module @@ -1009,12 +1010,16 @@ Used by `coq-goal-command-p'" (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 "\\`\\(Module\\)\\_>" str) + (affect (coq-count-match ":=" str)) + (case-fold-search nil)) + (and (string-match "\\`\\(Module\\)\\_>" str) (= letwith affect)))) (defun coq-section-command-p (str) - (proof-string-match "\\`\\(Section\\|Chapter\\)\\_>" str)) + (let ((case-fold-search nil)) + (string-match "\\`\\(Section\\|Chapter\\)\\_>" str))) + +(defvar coq-goal-command-regexp) ;; unused anymore (for good) (defun coq-goal-command-str-p (str) @@ -1023,16 +1028,17 @@ Use ‘coq-goal-command-p’ on a span instead if possible." (let* ((match (coq-count-match "\\_<match\\_>" str)) (with (- (coq-count-match "\\_<with\\_>" str) (coq-count-match "\\_<with\\s-+signature\\_>" str))) (letwith (+ (coq-count-match "\\_<let\\_>" str) (- with match))) - (affect (coq-count-match ":=" str))) - (and (proof-string-match coq-goal-command-regexp str) + (affect (coq-count-match ":=" str)) + (case-fold-search nil)) + (and (string-match coq-goal-command-regexp str) (not (and - (proof-string-match + (string-match (concat "\\`\\(Local\\|Definition\\|Lemma\\|Theorem\\|Fact\\|Add\\|Let\\|Program\\|Module\\|Class\\|Instance\\)\\_>") str) (not (= letwith affect)))) - (not (proof-string-match "\\`Declare\\s-+Module\\(\\w\\|\\s-\\|<\\)*:" - str))))) + (not (string-match "\\`Declare\\s-+Module\\(\\w\\|\\s-\\|<\\)*:" + str))))) ;; This is the function that tests if a SPAN is a goal start. All it ;; has to do is look at the 'goalcmd attribute of the span. @@ -1063,8 +1069,15 @@ It is used: (append coq-keywords-save-strict '("Proof")) ) +;; According to Coq, "Definition" is both a declaration and a goal. +;; 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) + "\\)"))) -(defun coq-save-command-p (span str) +(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) @@ -1151,8 +1164,10 @@ It is used: ;; FIXME: actually these are not exactly reserved keywords, find ;; another classification of keywords. (defvar coq-reserved-regexp - (concat "\\_<with\\s-+signature\\_>\\|" - (proof-ids-to-regexp coq-reserved))) + (concat "\\_<" + "\\(?:with\\s-+signature\\|" + (regexp-opt coq-reserved) "\\)" + "\\_>")) (defvar coq-state-changing-tactics (coq-build-regexp-list-from-db coq-tactics-db 'filter-state-changing)) @@ -1276,16 +1291,6 @@ It is used: "*Font-lock table for Coq terms.") - -;; According to Coq, "Definition" is both a declaration and a goal. -;; 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) - "\\)"))) - - (defconst coq-save-command-regexp (proof-anchor-regexp (concat "\\(?:Time\\s-+\\)?\\(" (proof-ids-to-regexp coq-keywords-save) @@ -1402,7 +1407,8 @@ part of another hypothesis.") (search-forward-regexp coq-hyp-name-or-goalsep-in-goal-or-response-regexp nil t) (goto-char (match-beginning 1)) ;; if previous is a newline, don't include it i the overklay - (when (looking-back "\\s-") (goto-char (- (point) 1))) + (when (looking-back "\\s-" (1- (point))) + (goto-char (- (point) 1))) (point)))) ; if several hyp names, we name the overlays with the first hyp name (setq res @@ -28,8 +28,6 @@ (require 'outline) (require 'newcomment) (require 'etags)) -(defvar smie-indent-basic) -(defvar smie-rules-function) (defvar proof-info) ; dynamic scope in proof-tree-urgent-action (defvar action) ; dynamic scope in coq-insert-as stuff (defvar string) ; dynamic scope in coq-insert-as stuff @@ -51,17 +49,6 @@ (require 'coq-seq-compile) ; sequential compilation of Requires (require 'coq-par-compile) ; parallel compilation of Requires -;; for compilation in Emacs < 23.3 (NB: declare function only works at top level) -(declare-function smie-bnf->prec2 "smie") -(declare-function smie-rule-parent-p "smie") -(declare-function smie-default-forward-token "smie") -(declare-function smie-default-backward-token "smie") -(declare-function smie-rule-prev-p "smie") -(declare-function smie-rule-separator "smie") -(declare-function smie-rule-parent "smie") - -(declare-function some "cl-extra") ; spurious bytecomp warning - ;; prettify is in emacs > 24.4 ;; FIXME: this should probably be done like for smie above. (defvar coq-may-use-prettify (fboundp 'prettify-symbols-mode)) @@ -331,17 +318,7 @@ See also option `coq-hide-additional-subgoals'." ;; Indentation and navigation support via SMIE. -(defcustom coq-use-smie t - "OBSOLETE. smie code is always used now. - -If non-nil, Coq mode will try to use SMIE for indentation. -SMIE is a navigation and indentation framework available in Emacs >= 23.3." - :type 'boolean - :group 'coq) - -(require 'smie nil 'noerror) -(require 'coq-smie nil 'noerror) - +(require 'coq-smie) ;; ;; Auxiliary code for Coq modes @@ -352,8 +329,8 @@ SMIE is a navigation and indentation framework available in Emacs >= 23.3." "Return a list of frames displaying both response and goals buffers." (let* ((wins-resp (get-buffer-window-list proof-response-buffer nil t)) (wins-gls (get-buffer-window-list proof-goals-buffer nil t)) - (frame-resp (cl-mapcar 'window-frame wins-resp)) - (frame-gls (cl-mapcar 'window-frame wins-gls))) + (frame-resp (mapcar #'window-frame wins-resp)) + (frame-gls (mapcar #'window-frame wins-gls))) (filtered-frame-list (lambda (x) (and (member x frame-resp) (member x frame-gls)))))) @@ -683,7 +660,7 @@ If locked span already has a state number, then do nothing. Also updates ;; This hook seems the one we want. ;; WARNING! It is applied once after each command PLUS once before a group of ;; commands is started -(add-hook 'proof-state-change-hook 'coq-set-state-infos) +(add-hook 'proof-state-change-hook #'coq-set-state-infos) (defun count-not-intersection (l notin) @@ -1028,7 +1005,7 @@ UNSETCMD. See `coq-command-with-set-unset'." (concat " -\"" s "\"")) (defun coq-build-removed-patterns (l) - (mapcar 'coq-build-removed-pattern l)) + (mapcar #'coq-build-removed-pattern l)) (defsubst coq-put-into-quotes (s) (concat "\"" s "\"")) @@ -1219,10 +1196,10 @@ Printing All set." (setq symb val) ;; FIXME this is wrong (it should be 'set', but it would set nil sometimes) (if coq-auto-adapt-printing-width (progn - (add-hook 'proof-assert-command-hook 'coq-adapt-printing-width) - (add-hook 'proof-retract-command-hook 'coq-reset-printing-width)) - (remove-hook 'proof-assert-command-hook 'coq-adapt-printing-width) - (remove-hook 'proof-retract-command-hook 'coq-reset-printing-width))) + (add-hook 'proof-assert-command-hook #'coq-adapt-printing-width) + (add-hook 'proof-retract-command-hook #'coq-reset-printing-width)) + (remove-hook 'proof-assert-command-hook #'coq-adapt-printing-width) + (remove-hook 'proof-retract-command-hook #'coq-reset-printing-width))) ;; In case of nested proofs (which are announced as obsolete in future versions ;; of coq) Coq does not show the goals of enclosing proof when closing a nested @@ -1258,13 +1235,13 @@ be called and no command will be sent to Coq." ;; silent (there is no goal to show). (string-match "Backtrack" cmd)) (list "Unset Silent.")))) - + (defpacustom auto-adapt-printing-width t "If non-nil, adapt automatically printing width of goals window. Each timme the user sends abunch of commands to Coq, check if the width of the goals window changed, and adapt coq printing width. WARNING: If several windows are displaying the goals buffer, one -is chosen randomly. WARNING 2: when backtracking the printing +is chosen arbitrarily. WARNING 2: when backtracking the printing width is synchronized by coq (?!)." :type 'boolean :safe 'booleanp @@ -1278,7 +1255,7 @@ width is synchronized by coq (?!)." ;; this initiates auto adapt printing width at start, by reading the config ;; var. Let us put this at the end of hooks to have a chance to read local ;; variables first. -(add-hook 'coq-mode-hook 'coq-auto-adapt-printing-width t) +(add-hook 'coq-mode-hook #'coq-auto-adapt-printing-width t) (defvar coq-shell-current-line-width nil "Current line width of the Coq printing width. @@ -1559,10 +1536,10 @@ use `coq-unhighlight-hyp' to unhilight." (coq-unhighlight-hyp-aux h))) (defun coq-highlight-hyps (lh) - (mapc 'coq-highlight-hyp lh)) + (mapc #'coq-highlight-hyp lh)) (defun coq-unhighlight-hyps (lh) - (mapc 'coq-unhighlight-hyp-aux lh)) + (mapc #'coq-unhighlight-hyp-aux lh)) (defun coq-highlight-selected-hyps () "Highlight all hyps stored in `coq-highlighted-hyps'. @@ -1597,7 +1574,7 @@ See `coq-highlight-hyps-cited-in-response' and `SearchAbout'." Highlight always takes place in goals buffer." (let ((inters (coq-get-hyps-cited-in-response))) (coq-unhighlight-selected-hyps) - (setq coq-highlighted-hyps (mapcar 'car inters)) + (setq coq-highlighted-hyps (mapcar #'car inters)) (coq-highlight-selected-hyps))) (defun coq-toggle-highlight-hyp (h) @@ -1734,12 +1711,12 @@ See `coq-fold-hyp'." (defun coq-unfold-hyp-list (lh) "Fold the type of hypothesis in LH temporarily. See `coq-unfold-hyp-aux'." - (mapc 'coq-unfold-hyp-aux lh)) + (mapc #'coq-unfold-hyp-aux lh)) (defun coq-fold-hyp-list (lh) "Fold the type of hypothesis in LH temporarily. See `coq-fold-hyp-aux'." - (mapc 'coq-fold-hyp-aux lh)) + (mapc #'coq-fold-hyp-aux lh)) (defun coq-fold-hyps () "Fold the type of hypothesis in LH durably. @@ -1828,7 +1805,6 @@ See `coq-fold-hyp'." ;; *default* value to nil. (custom-set-default 'proof-output-tooltips nil) -;; This seems xemacs only code, remove? (defconst coq-prettify-symbols-alist '(("not" . ?¬) ;; ("/\\" . ?∧) @@ -1957,7 +1933,7 @@ Near here means PT is either inside or just aside of a comment." (setq proof-assistant-home-page coq-www-home-page) (setq proof-prog-name coq-prog-name) - (setq proof-guess-command-line 'coq-guess-command-line) + (setq proof-guess-command-line #'coq-guess-command-line) (setq proof-prog-name-guess t) ;; We manage file saveing via coq-compile-auto-save and for coq @@ -1982,26 +1958,25 @@ Near here means PT is either inside or just aside of a comment." '(coq-compile-quick coq-compile-keep-going coq-compile-auto-save coq-lock-ancestors)) - (setq proof-goal-command-p 'coq-goal-command-p - proof-find-and-forget-fn 'coq-find-and-forget - pg-topterm-goalhyplit-fn 'coq-goal-hyp - proof-state-preserving-p 'coq-state-preserving-p) + (setq proof-goal-command-p #'coq-goal-command-p + proof-find-and-forget-fn #'coq-find-and-forget + pg-topterm-goalhyplit-fn #'coq-goal-hyp + proof-state-preserving-p #'coq-state-preserving-p) (setq proof-query-identifier-command "Check %s.") ;;TODO: from v8.5 this wold be better: ;;(setq proof-query-identifier-command "About %s.") (setq proof-save-command-regexp coq-save-command-regexp - proof-really-save-command-p 'coq-save-command-p ;pierre:deals with Proof <term>. + proof-really-save-command-p #'coq-save-command-p ;pierre:deals with Proof <term>. proof-save-with-hole-regexp coq-save-with-hole-regexp proof-goal-with-hole-regexp coq-goal-with-hole-regexp proof-nested-undo-regexp coq-state-changing-commands-regexp proof-script-imenu-generic-expression coq-generic-expression) - (when (fboundp 'smie-setup) ; always use smie, old indentation code removed - (smie-setup coq-smie-grammar #'coq-smie-rules - :forward-token #'coq-smie-forward-token - :backward-token #'coq-smie-backward-token)) + (smie-setup coq-smie-grammar #'coq-smie-rules + :forward-token #'coq-smie-forward-token + :backward-token #'coq-smie-backward-token) ;; old indentation code. ;; (require 'coq-indent) @@ -2060,7 +2035,7 @@ Near here means PT is either inside or just aside of a comment." (setq proof-cannot-reopen-processed-files nil) - (add-hook 'proof-activate-scripting-hook 'proof-cd-sync nil t)) + (add-hook 'proof-activate-scripting-hook #'proof-cd-sync nil t)) (defun coq-shell-mode-config () (setq @@ -2190,13 +2165,13 @@ Near here means PT is either inside or just aside of a comment." ; -;;; FIXME: to handle "printing all" properly, we should change the state -;;; of the variables that also depend on it. -;;; da: +;; FIXME: to handle "printing all" properly, we should change the state +;; of the variables that also depend on it. +;; da: -;;; pc: removed it and others of the same kind. Put an "option" menu instead, -;;; with no state variable. To have the state we should use coq command that -;;; output the value of the variables. +;; pc: removed it and others of the same kind. Put an "option" menu instead, +;; with no state variable. To have the state we should use coq command that +;; output the value of the variables. ;(defpacustom print-fully-explicit nil ; "Print fully explicit terms." ; :type 'boolean @@ -2326,7 +2301,7 @@ The not yet delayed output is in the region proof-tree-show-subgoal)) proof-action-list)))))))))) -(add-hook 'proof-tree-urgent-action-hook 'coq-proof-tree-get-new-subgoals) +(add-hook 'proof-tree-urgent-action-hook #'coq-proof-tree-get-new-subgoals) (defun coq-find-begin-of-unfinished-proof () @@ -2455,7 +2430,7 @@ result of `coq-proof-tree-get-proof-info'." ;; finished the current proof (coq-proof-tree-disable-evars))))) -(add-hook 'proof-tree-urgent-action-hook 'coq-proof-tree-evar-display-toggle) +(add-hook 'proof-tree-urgent-action-hook #'coq-proof-tree-evar-display-toggle) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -2479,7 +2454,7 @@ result of `coq-proof-tree-get-proof-info'." (coq-bullet-p string)) ;; coq does not accept "Time -". (setq string (concat coq--time-prefix string)))))) -(add-hook 'proof-shell-insert-hook 'coq-preprocessing) +(add-hook 'proof-shell-insert-hook #'coq-preprocessing) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; @@ -2533,8 +2508,8 @@ mouse activation." (string-match-p "\\.v\\'" s)) (defun coq-directories-files (l) - (let* ((file-list-list (mapcar 'directory-files l)) - (file-list (apply 'append file-list-list)) + (let* ((file-list-list (mapcar #'directory-files l)) + (file-list (apply #'append file-list-list)) (filtered-list (cl-remove-if-not #'coq-postfix-.v-p file-list))) filtered-list)) @@ -2549,7 +2524,7 @@ mouse activation." (cleanpth (mapcar #'coq-load-path-to-paths pth)) (existingpth (cl-remove-if-not #'file-exists-p cleanpth)) (file-list (coq-directories-files existingpth))) - (mapcar 'coq-remove-dot-v-extension file-list))) + (mapcar #'coq-remove-dot-v-extension file-list))) (defun coq-insert-section-or-module () "Insert a module or a section after asking right questions." @@ -3005,7 +2980,7 @@ buffer." (defun coq-highlight-error-hook () (coq-highlight-error t t)) -(add-hook 'proof-shell-handle-error-or-interrupt-hook 'coq-highlight-error-hook t) +(add-hook 'proof-shell-handle-error-or-interrupt-hook #'coq-highlight-error-hook t) ;; @@ -3102,9 +3077,9 @@ number of hypothesis displayed, without hiding the goal" ;; This hook must be added before coq-optimise-resp-windows, in order to be evaluated ;; *after* windows resizing. (add-hook 'proof-shell-handle-delayed-output-hook - 'coq-show-first-goal) + #'coq-show-first-goal) (add-hook 'proof-shell-handle-delayed-output-hook - 'coq-update-minor-mode-alist) + #'coq-update-minor-mode-alist) (add-hook 'proof-shell-handle-delayed-output-hook (lambda () (if (proof-string-match coq-shell-proof-completed-regexp @@ -3124,7 +3099,7 @@ number of hypothesis displayed, without hiding the goal" (<= (- (frame-height) (window-height)) 2)) ;; bug fixed in generic ocde, useless now: -;(add-hook 'proof-activate-scripting-hook '(lambda () (when proof-three-window-enable (proof-layout-windows)))) +;(add-hook 'proof-activate-scripting-hook (lambda () (when proof-three-window-enable (proof-layout-windows)))) ;; *Experimental* auto shrink response buffer in three windows mode. Things get ;; a bit messed up if the response buffer is not at the right place (below @@ -3174,9 +3149,11 @@ Only when three-buffer-mode is enabled." ;; i.e. added in hook AFTER it. ;; Adapt when displaying a normal message -(add-hook 'proof-shell-handle-delayed-output-hook 'coq-optimise-resp-windows-if-option) +(add-hook 'proof-shell-handle-delayed-output-hook + #'coq-optimise-resp-windows-if-option) ;; Adapt when displaying an error or interrupt -(add-hook 'proof-shell-handle-error-or-interrupt-hook 'coq-optimise-resp-windows-if-option) +(add-hook 'proof-shell-handle-error-or-interrupt-hook + #'coq-optimise-resp-windows-if-option) ;;; DOUBLE HIT ELECTRIC TERMINATOR ;; Trying to have double hit on colon behave like electric terminator. The "." @@ -3306,7 +3283,7 @@ priority to the former." ;; when "compile when require" is off. When switching scripting buffer, let us ;; restart the coq shell process, so that it applies local coqtop options. (add-hook 'proof-deactivate-scripting-hook - 'coq-switch-buffer-kill-proof-shell ;; this function is in coq-compile-common + #'coq-switch-buffer-kill-proof-shell ;; this function is in coq-compile-common t) |