From a36eb9bed9b8f7f63943fd2e0d505ad34e426136 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
Date: Tue, 10 Sep 2024 10:23:17 +0200
Subject: [PATCH] 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(-)
 create mode 100644 ci/test-indent/indent-backslash-ops.v

diff --git a/ci/test-indent/indent-backslash-ops.v b/ci/test-indent/indent-backslash-ops.v
new file mode 100644
index 000000000..5af155645
--- /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 d944e9495..5528c6558 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