diff options
| author | Erik Martin-Dorel | 2019-12-08 01:32:28 +0100 |
|---|---|---|
| committer | Erik Martin-Dorel | 2019-12-08 14:23:58 +0100 |
| commit | 986fefde8e2f5b942f9715b4e423c6a350497004 (patch) | |
| tree | 5693436fb30135fccf170cf7b15991b5c5dee0fd /coq | |
| parent | b893f682a9bbd0f42dfd4501dc0451ab1e4ec713 (diff) | |
fix: Recognize "Timeout" before save keywords
viz. '("Defined" "Save" "Qed" "End" "Admitted" "Abort" "Proof")
Diffstat (limited to 'coq')
| -rw-r--r-- | coq/coq-syntax.el | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index b5cd1ec2..93db1a77 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -1070,7 +1070,7 @@ It is used: ;; It is understood here as being a goal. This is important for ;; recognizing global identifiers, see coq-global-p. (defconst coq-save-command-regexp-strict - (concat "\\`\\(?:Time\\s-+\\)?\\(" + (concat "\\`\\(?:Time\\s-+\\|Timeout\\s-+[[:digit:]]+\\s-+\\)*\\(" "\\_<" (regexp-opt coq-keywords-save-strict) "\\_>" @@ -1293,12 +1293,13 @@ It is used: (defconst coq-save-command-regexp ;; FIXME: The surrounding grouping parens are probably not needed. - (concat "\\`\\(\\(?:Time\\s-+\\)?\\_<" + (concat "\\`\\(\\(?:Time\\s-+\\|Timeout\\s-+[[:digit:]]+\\s-+\\)*\\_<" (regexp-opt coq-keywords-save t) "\\_>\\)")) (defconst coq-save-with-hole-regexp - (concat "\\(?:Time\\s-+\\)?\\(" (regexp-opt coq-keywords-save-strict) + (concat "\\(?:Time\\s-+\\|Timeout\\s-+[[:digit:]]+\\s-+\\)*\\(" + (regexp-opt coq-keywords-save-strict) "\\)\\s-+\\(" coq-id "\\)\\s-*\\.")) (defconst coq-goal-command-regexp |