[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[nongnu] elpa/proof-general ce033327e3 4/8: Support for command "Derive
From: |
ELPA Syncer |
Subject: |
[nongnu] elpa/proof-general ce033327e3 4/8: Support for command "Derive SuchThat As". |
Date: |
Tue, 29 Mar 2022 02:58:42 -0400 (EDT) |
branch: elpa/proof-general
commit ce033327e30971b28c0cf67655f3aed86cbb329a
Author: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
Commit: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
Support for command "Derive SuchThat As".
Indentation + syntax highlighting.
---
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.")
- [nongnu] elpa/proof-general updated (40c40d229e -> e1e29acb04), ELPA Syncer, 2022/03/29
- [nongnu] elpa/proof-general 3c9bed7061 1/8: Add an option to stop proof-shell-kill-function from killing buffers., ELPA Syncer, 2022/03/29
- [nongnu] elpa/proof-general 39911fe049 2/8: Fix #646. Indentation of function arguments., ELPA Syncer, 2022/03/29
- [nongnu] elpa/proof-general 1554eb7936 6/8: Merge pull request #648 from Matafou/fix-#599-Proof-using-bad-detection, ELPA Syncer, 2022/03/29
- [nongnu] elpa/proof-general e1e29acb04 8/8: Merge pull request #639 from Chobbes/save-frames, ELPA Syncer, 2022/03/29
- [nongnu] elpa/proof-general 24da4f5593 3/8: Fix #599, bad detection of "Proof" in "Proof using" suggestions., ELPA Syncer, 2022/03/29
- [nongnu] elpa/proof-general 17a4cc00d6 5/8: Merge pull request #649 from Matafou/fix-#618-missing-keyword-derive, ELPA Syncer, 2022/03/29
- [nongnu] elpa/proof-general ce033327e3 4/8: Support for command "Derive SuchThat As".,
ELPA Syncer <=
- [nongnu] elpa/proof-general 0b3454492c 7/8: Merge pull request #647 from Matafou/fix-#646-indent-funargs, ELPA Syncer, 2022/03/29