From 05e3dc3ad4482a166be120b65930f9b5aa19d8db Mon Sep 17 00:00:00 2001 From: Columbus240 <8899730+Columbus240@users.noreply.github.com> Date: Mon, 6 Nov 2023 09:23:03 +0100 Subject: [PATCH 1/2] Remove duplicate def. of `coq-looking-at-comment` --- coq/coq-indent.el | 5 ----- 1 file changed, 5 deletions(-) diff --git a/coq/coq-indent.el b/coq/coq-indent.el index e4f72c036..b1e3e0425 100644 --- a/coq/coq-indent.el +++ b/coq/coq-indent.el @@ -264,11 +264,6 @@ if found, to (point-max) otherwise. Return t if found, nil otherwise." (setq nbopen (- nbopen 1)))) (= nbopen 0)))) -(defun coq-looking-at-comment () - "Return non-nil if point is inside a comment." - (or (proof-inside-comment (point)) - (proof-inside-comment (+ 1 (point))))) - (defun coq-find-comment-start () "Go to the current comment start. If inside nested comments, go to the start of the outer most comment. From 39f967e5ef5c8d4dfed3419138026cb02ebff71d Mon Sep 17 00:00:00 2001 From: Columbus240 <8899730+Columbus240@users.noreply.github.com> Date: Mon, 6 Nov 2023 15:56:50 +0100 Subject: [PATCH 2/2] Change _CoqProject separator settings According to the code of coq_makefile, `\r` is not considered white-space in _CoqProject. (https://github.com/coq/coq/blob/a7f51315db5d70888af3b96a579eb799a2b45ca9/lib/coqProject_file.ml#L84) --- coq/coq-system.el | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/coq/coq-system.el b/coq/coq-system.el index 28c9dce4f..ad65cc4bc 100644 --- a/coq/coq-system.el +++ b/coq/coq-system.el @@ -550,7 +550,7 @@ alreadyopen is t if buffer already existed." (find-file-noselect projectfile t t)))) (list projectbuffer projectbufferalreadyopen)))))) -(defconst coq--project-file-separator "[\r\n[:space:]]+") +(defconst coq--project-file-separator "[\r\t\n[:space:]]+") (defconst coq--makefile-switch-arities '(("-R" . 2)