diff options
author | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2017-10-26 14:13:09 +0200 |
---|---|---|
committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2017-10-26 14:13:09 +0200 |
commit | fa0da5b062f7d76f1cd1bc51b291e6fc62092b66 (patch) | |
tree | d5adac693cdc02fde7c5b389973f2ab5cf847701 | |
parent | 9083698d0bbd4438208fa72222438ae59684542d (diff) |
Limited extensibility of smie token detection.
-rw-r--r-- | coq/coq-smie.el | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/coq/coq-smie.el b/coq/coq-smie.el index 33ef19d1..11952b68 100644 --- a/coq/coq-smie.el +++ b/coq/coq-smie.el @@ -42,6 +42,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. @@ -375,6 +388,9 @@ The point should be at the beginning of the command name." (defun coq-smie-forward-token () (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 @@ -492,6 +508,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 ",") |