From 017d4b516713622a160eb6786c2bde5f7f6ee91e Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Wed, 15 Apr 2020 22:08:26 +0200 Subject: Fix a bug in detection of "Proof." when "proof using" insertion --- coq/coq.el | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'coq') diff --git a/coq/coq.el b/coq/coq.el index 5dc45a9a..cb43f3a9 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -2622,9 +2622,13 @@ Remarks and limitations: "Coq specific additional menu entry for \"Proof using\". annotation. See `proof-dependency-menu-system-specific'." ) +(defconst coq-proof-using-regexp "\\_\\)?\\([^.]*\\)\\." + "regexp matching Coq \"Proof( using xxx)?.\" annotation. +There should be one subexp numbered 1 matching xxx if present.") + (defun coq-mark-span-dependencies (span suggested) (goto-char (span-start span)) - (let* ((endpos (re-search-forward "\\\\([^.]*\\)\\.")) + (let* ((endpos (re-search-forward coq-proof-using-regexp)) (proof-pos (match-beginning 0)) (newspan (span-make proof-pos endpos))) (span-set-property newspan 'face 'proof-warning-face) @@ -2657,7 +2661,7 @@ built from the list of strings in SUGGESTED." (with-current-buffer proof-script-buffer (save-excursion (goto-char (span-start span)) - (let* ((endpos (re-search-forward "\\\\([^.]*\\)\\."))) + (let* ((endpos (re-search-forward coq-proof-using-regexp))) (when endpos (let* ((suggested (span-property span 'dependencies)) (proof-pos (match-beginning 0)) -- cgit v1.2.3