[nongnu] elpa/proof-general 17a4cc00d6 5/8: Merge pull request #649 from Matafou/fix-#618-missing-keyword-derive

[ELPA Syncer]

branch: elpa/proof-general
commit 17a4cc00d62a41b1abd196e463e029dd65fd1ca7
Merge: 40c40d229e ce033327e3
Author: Pierre Courtieu <Matafou@users.noreply.github.com>
Commit: GitHub <noreply@github.com>

    Merge pull request #649 from Matafou/fix-#618-missing-keyword-derive
    
    Fix #618 - Support for command "Derive SuchThat As".
---
 coq/coq-smie.el   | 12 ++++++++++++
 coq/coq-syntax.el |  8 +++++++-
 2 files changed, 19 insertions(+), 1 deletion(-)

diff --git a/coq/coq-smie.el b/coq/coq-smie.el
index 5d6c4fccda..79bc3ab85e 100644
--- a/coq/coq-smie.el
+++ b/coq/coq-smie.el
@@ -452,6 +452,12 @@ The point should be at the beginning of the command name."
 (defun coq-is-cmdend-token (tok)
   (or (coq-is-bullet-token tok) (coq-is-subproof-token tok) (coq-is-dot-token 
tok)))
 
+;; Standard synonyms are better here than in the coq-smie-xxxward-token-aux 
functions.
+(defconst coq-standard-token-synonyms
+  '(
+    ("SuchThat" . ":") ("As" . ":= def") ;; For "Derive foo SuchThat bar As 
oof".
+    ))
+
 (defun coq-smie-forward-token ()
   (let ((tok (coq-smie-forward-token-aux)))
     (cond
@@ -461,6 +467,9 @@ The point should be at the beginning of the command name."
      ((assoc tok coq-smie-monadic-tokens)
       (let ((res (assoc tok coq-smie-monadic-tokens)))
         (cdr res)))
+     ((assoc tok coq-standard-token-synonyms)
+      (let ((res (assoc tok coq-standard-token-synonyms)))
+        (cdr res)))
      (tok))))
 
 (defun coq-smie-forward-token-aux ()
@@ -639,6 +648,9 @@ The point should be at the beginning of the command name."
      ((assoc tok coq-smie-monadic-tokens)
       (let ((res (assoc tok coq-smie-monadic-tokens)))
         (cdr res)))
+     ((assoc tok coq-standard-token-synonyms)
+      (let ((res (assoc tok coq-standard-token-synonyms)))
+        (cdr res)))
      (tok))))
 
 (defun coq-smie-backward-token-aux ()
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 5017a6ed32..68c10abd19 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -477,6 +477,7 @@ so for the following reasons:
     ("Derive Inversion" nil "Derive Inversion @{id} with # Sort #." t 
"Derive\\s-+Inversion")
     ("Derive Dependent Inversion" nil "Derive Dependent Inversion @{id} with # 
Sort #." t "Derive\\s-+Dependent\\s-+Inversion")
     ("Derive Inversion_clear" nil "Derive Inversion_clear @{id} with # Sort 
#." t)
+    ("Derive SuchThat" nil "Derive @[id] SuchThat # As @{id}." t "Derive")
     ("Example" "ex" "Example #:# := #." t "Example");; careful
     ("Equations" "eqs" "Equations #:# := #." t "Equations")
     ("Fixpoint" "fix" "Fixpoint # (#:#) {struct @{arg}} : # :=\n#." t 
"Fixpoint")
@@ -1207,7 +1208,12 @@ different."
      "using" "with" "beta" "delta" "iota" "zeta" "after" "until"
      "at" "Sort" "Time" "dest" "where"
      ;; SSReflect user reserved.
-     "is" "nosimpl" "of")
+     "is" "nosimpl" "of"
+     ;; Derive reserved
+     "SuchThat" "As" ;; I don't like these two: they start with
+                     ;; capitals but they are not at beginning of a
+                     ;; sentence
+     )
    coq-user-reserved-db)
   "Reserved keywords of Coq.")