branch: elpa/proof-general
commit a36eb9bed9b8f7f63943fd2e0d505ad34e426136
Author: Pierre Courtieu <pierre.court...@cnam.fr>
Commit: Pierre Courtieu <pierre.court...@cnam.fr>
Fix #757 indentation of "\in"
The lexer now glues a "\" to an immediately following word if it is
itself preceded by a space.
Note that for really good indentation you should try to add something
like this to your configuration:
(setq coq-smie-user-tokens '(("\\in" . "=")))
to tell the indentation grammar that \in has the same precedence as
"=".
Test added.
---
ci/test-indent/indent-backslash-ops.v | 23 +++++++++++++++++++++++
coq/coq-smie.el | 35 +++++++++++++++++++++++++++++++----
2 files changed, 54 insertions(+), 4 deletions(-)
diff --git a/ci/test-indent/indent-backslash-ops.v
b/ci/test-indent/indent-backslash-ops.v
new file mode 100644
index 0000000000..5af1556458
--- /dev/null
+++ b/ci/test-indent/indent-backslash-ops.v
@@ -0,0 +1,23 @@
+Require Import mathcomp.ssreflect.ssrbool.
+
+Definition xx := nat.
+Module foo.
+ (* from PG issue #757 *)
+ Lemma test:
+ forall a : nat,
+ a \in [::] -> (* "\in" should be detected as one token *)
+ False.
+ Proof.
+ Abort.
+ Qed.
+
+ Lemma test2:
+ forall a : nat,
+ a \in (* "\in" should be detected as one token *)
+ [::] ->
+ False.
+ Proof.
+ Abort.
+ Qed.
+End foo.
+
diff --git a/coq/coq-smie.el b/coq/coq-smie.el
index d944e94958..5528c65586 100644
--- a/coq/coq-smie.el
+++ b/coq/coq-smie.el
@@ -266,14 +266,18 @@ the token of \".\" is simply \".\"."
;; A variant of smie-default-backward-token that recognize "." and ";"
-;; as single token even if glued at the end of another symbols.
-
+;; as single token even if glued at the end of another symbols. We
+;; glue "\" in front of a word though, to follow ssreflects
+;; ocnvention.
(defun coq-backward-token-fast-nogluing-dot-friends ()
(forward-comment (- (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_'"))
+ ;; skip a regular word + one backslash
+ (when (zerop tok-punc)
+ (skip-syntax-backward "w_'")
+ (if (looking-back "\\s-\\\\") (forward-char -1)))
;; 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))
@@ -286,7 +290,9 @@ the token of \".\" is simply \".\"."
(let* ((pt (point))
(tok-punc (skip-syntax-forward "."))
(str-punc (buffer-substring-no-properties pt (point))))
- (if (zerop tok-punc) (skip-syntax-forward "w_'"))
+ (if (or (zerop tok-punc) (string-match "\\\\" str-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))
@@ -653,6 +659,27 @@ The point should be at the beginning of the command name."
(cdr res)))
(tok))))
+;; Modified from smie.el
+(defun smie-default-forward-token ()
+ (forward-comment (point-max))
+ (buffer-substring-no-properties
+ (point)
+ (let ((dist (skip-syntax-forward ".")))
+
+ (when (or (zerop dist)
+ (and (= 1 dist) (looking-back "\\\\")))
+ (skip-syntax-forward "w_'"))
+ (point))))
+
+(defun smie-default-backward-token ()
+ (forward-comment (- (point)))
+ (buffer-substring-no-properties
+ (point)
+ (progn (when (zerop (skip-syntax-backward "."))
+ (skip-syntax-backward "w_'")
+ (if (looking-back "\\s-\\\\") (forward-char -1)))
+ (point))))
+
(defun coq-smie-backward-token-aux ()
(let* ((tok (smie-default-backward-token)))
(cond
