diff options
Diffstat (limited to 'coq/coq-smie.el')
| -rw-r--r-- | coq/coq-smie.el | 60 |
1 files changed, 53 insertions, 7 deletions
diff --git a/coq/coq-smie.el b/coq/coq-smie.el index 33ef19d1..59d84e36 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: @@ -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. @@ -375,6 +396,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 @@ -481,7 +505,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 +516,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 ",") @@ -567,12 +594,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") @@ -599,6 +642,9 @@ The point should be at the beginning of the command name." ((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")) |