diff options
Diffstat (limited to 'coq/coq-smie.el')
| -rw-r--r-- | coq/coq-smie.el | 136 |
1 files changed, 92 insertions, 44 deletions
diff --git a/coq/coq-smie.el b/coq/coq-smie.el index c488e73f..15697354 100644 --- a/coq/coq-smie.el +++ b/coq/coq-smie.el @@ -1,10 +1,18 @@ ;;; coq-smie.el --- SMIE lexer, grammar, and indent rules for Coq -;; Copyright (C) 2014 Free Software Foundation, Inc +;; 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 2001-2017 Pierre Courtieu +;; Portions © Copyright 2010, 2016 Erik Martin-Dorel +;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews +;; Portions © Copyright 2015-2017 Clément Pit-Claudel ;; Authors: Pierre Courtieu ;; Stefan Monnier ;; Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr> + ;; License: GPLv3+ (GNU GENERAL PUBLIC LICENSE version 3 or later) ;;; Commentary: @@ -12,7 +20,7 @@ ;; Lexer. ;; Due to the verycomplex grammar of Coq, and to the architecture of -;; smie, we deambiguate all kinds of tokens during lexing. This is a +;; smie, we deambiguate all kinds of tokens during lexing. This is a ;; complex piece of code but it allows for all smie goodies. ;; Some examples of deambigations: ;; - We distinguish ":=" from ":= inductive" to avoid the circular precedence @@ -42,6 +50,19 @@ ; ,@body ; (message "%.06f" (float-time (time-since time))))) +(defcustom coq-smie-user-tokens nil + "Alist of (syntax . token) pairs to extend the coq smie parser. +These are user configurable additional syntax for smie tokens. It +allows to define alternative syntax for smie token. Typical +example: if you define a infix operator \"xor\" you may want to +define it as a new syntax for token \"or\" in order to have the +indentation rules of or applied to xor. Other exemple: if you +want to define a new notation \"ifb\" ... \"then\" \"else\" then +you need to declare \"ifb\" as a new syntax for \"if\" to make +indentation work well." + :type '(alist :key-type string :value-type string) + :group 'coq) + (defun coq-string-suffix-p (str1 str2 &optional ignore-case) "Return non-nil if STR1 is a prefix of STR2. @@ -92,7 +113,7 @@ attention to case differences." (defun coq-smie-is-ltacdef () (let ((case-fold-search nil)) - (save-excursion + (save-excursion (coq-find-real-start) (looking-at "\\(\\(Local\\|Global\\)\\s-+\\)?\\(Ltac\\|Tactic\\s-+Notation\\)\\s-")))) @@ -216,11 +237,11 @@ the token of \".\" is simply \".\"." ;; tokens and ignore-bteween are not disjoint (defun coq-smie-search-token-forward (tokens &optional end ignore-between) "Search for one of TOKENS between point and END. -If some enclosing parenthesis is reached, stop there and return -nil. Token \".\" is considered only if followed by a space. -optional IGNORE-BETWEEN defines opener/closer to ignore during -search. Careful: the search for a opener stays inside the current -command (and inside parenthesis)." +If some enclosing parenthesis is reached, stop there and return nil. +Token \".\" is considered only if followed by a space. Optional +IGNORE-BETWEEN defines opener/closer to ignore during search. +Careful: the search for a opener stays inside the current command (and +inside parenthesis)." (unless end (setq end (point-max))) (condition-case nil (catch 'found @@ -261,11 +282,12 @@ command (and inside parenthesis)." ;; tokens and ignore-bteween are not disjoint (defun coq-smie-search-token-backward (tokens &optional end ignore-between) "Search for one of TOKENS between point and END. -If some enclosing parenthesis is reached, stop there and return -nil. Token \".\" is considered only if followed by a space. +If some enclosing parenthesis is reached, stop there and return nil. +Token \".\" is considered only if followed by a space. optional IGNORE-BETWEEN defines opener/closer to ignore during -search. Careful: the search for a opener stays inside the current -command (and inside parenthesis). " +search. +Careful: the search for a opener stays inside the current command (and +inside parenthesis)." (unless end (setq end (point-min))) (condition-case nil (catch 'found @@ -322,9 +344,9 @@ proof-mode starter in Coq." ;; each goal anyway. (defun coq-smie-detect-goal-command () "Return t if the next command is a goal starting to be indented. -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 +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\\)?\ @@ -341,7 +363,7 @@ force indentation." 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) + ((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"))))) @@ -373,8 +395,11 @@ The point should be at the beginning of the command name." (defun coq-smie-forward-token () - (let ((tok (coq-forward-token-fast-nogluing-dot-friends))) + (let ((tok (smie-default-forward-token))) (cond + ((assoc tok coq-smie-user-tokens) + (let ((res (assoc tok coq-smie-user-tokens))) + (cdr res))) ;; @ may be ahead of an id, it is part of the id. ((and (equal tok "@") (looking-at "[[:alpha:]_]")) (let ((newtok (coq-smie-forward-token))) ;; recursive call @@ -481,7 +506,7 @@ The point should be at the beginning of the command name." ":= with" (goto-char p) ":= module"))) - ((member corresp '("Inductive" "CoInductive")) ":= inductive") + ((member corresp '("Inductive" "CoInductive" "Variant")) ":= inductive") ((equal corresp "let") ":= let") ((equal corresp "where") ":= inductive") ;; inductive or fixpoint, nevermind ((or (looking-back "{" nil)) ":= record") @@ -492,6 +517,9 @@ The point should be at the beginning of the command name." (defun coq-smie-backward-token () (let* ((tok (smie-default-backward-token))) (cond + ((assoc tok coq-smie-user-tokens) + (let ((res (assoc tok coq-smie-user-tokens))) + (cdr res))) ;; Distinguish between "," from quantification and other uses of ;; "," (tuples, tactic arguments) ((equal tok ",") @@ -530,7 +558,7 @@ 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) (looking-back "(" nil)) "||") ((equal backtok nil) (if (or (looking-back "\\[" nil) (and (looking-back "{" nil) @@ -567,12 +595,28 @@ The point should be at the beginning of the command name." (goto-char (1- (point))) "{|") ((and (zerop (length tok)) (member (char-before) '(?\{ ?\})) - (save-excursion - (forward-char -1) - (let ((nxttok (coq-smie-backward-token))) ;; recursive call - (coq-is-cmdend-token nxttok)))) + (save-excursion + (forward-char -1) + (if (and (looking-at "{") + (looking-back "\\([0-9]+\\s-*:\\s-*\\)" nil t)) + (goto-char (match-beginning 0))) + (let ((nxttok (coq-smie-backward-token))) ;; recursive call + (coq-is-cmdend-token nxttok)))) (forward-char -1) - (if (looking-at "{") "{ subproof" "} subproof")) + (if (looking-at "}") "} subproof" + (if (and (looking-at "{") + (looking-back "\\([0-9]+\\s-*:\\s-*\\)" nil t)) + (goto-char (match-beginning 0))) + "{ subproof" + )) + + ;; ((and (zerop (length tok)) (member (char-before) '(?\{ ?\})) + ;; (save-excursion + ;; (forward-char -1) + ;; (let ((nxttok (coq-smie-backward-token))) ;; recursive call + ;; (coq-is-cmdend-token nxttok)))) + ;; (forward-char -1) + ;; (if (looking-at "{") "{ subproof" "} subproof")) ((and (equal tok ":") (looking-back "\\<\\(constr\\|ltac\\|uconstr\\)" nil)) ": ltacconstr") @@ -592,9 +636,16 @@ The point should be at the beginning of the command name." ;; FIXME: no token should end with "." except "." itself ; for "unfold in *|-*." - ((member tok '("*." "-*." "|-*." "*|-*.")) (forward-char 1) ".") + ((member tok '("*." "-*." "|-*." "*|-*.")) + (forward-char (- (length tok) 1)) + (coq-smie-.-deambiguate)) ; for "unfold in *|-*;" - ((member tok '("*;" "-*;" "|-*;" "*|-*;")) (forward-char 1) "; tactic") ;; FIXME; can be "; ltac" too + ((member tok '("*;" "-*;" "|-*;" "*|-*;")) + ;; FIXME; can be "; ltac" too + (forward-char (- (length tok) 1)) "; tactic") + ;; bullet detected, is it really a bullet? we have to traverse + ;; recursively any other bullet or "n:{" "}". this is the work of + ;; coq-empty-command-p ((and (string-match coq-bullet-regexp-nospace tok) (save-excursion (coq-empty-command-p))) (concat tok " bullet")) @@ -719,8 +770,7 @@ Lemma foo: forall n, instead of: Lemma foo: forall n, - n = n. -" + n = n." :type 'boolean :group 'coq) @@ -734,19 +784,18 @@ Lemma foo: forall n, :safe #'coq-indent-safep) (defcustom coq-indent-semicolon-tactical 2 - "Number of spaces used to indent after the first tactical semi colon of a serie. - If set to 0, indetation is as follows: - tac1; - tac2; - tac3; - tac4. - - if set to 2 (default): - - tac1; - tac2; - tac3; - tac4." + "Number of spaces used to indent after the 1st tactical semicolon of a serie. +If set to 0, indentation is as follows: +tac1; +tac2; +tac3; +tac4. + +If set to 2 (default): +tac1; + tac2; + tac3; + tac4." :type 'integer :group 'coq :safe #'coq-indent-safep) @@ -770,8 +819,7 @@ for example, if set to 0 the indentation is as follows: If it is set to 2 (default) it is as follows: Lemma foo: forall x:nat, - x <= 0 -> x = 0. -" + x <= 0 -> x = 0." :type 'integer :group 'coq :safe #'coq-indent-safep) @@ -956,7 +1004,7 @@ Typical values are 2 or 4." ;; copied from elixir-smie.el (defun coq-smie--same-line-as-parent (parent-pos child-pos) - "Return non-nil if `child-pos' is on same line as `parent-pos'." + "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))) (defun coq-smie-rules (kind token) |