diff options
Diffstat (limited to 'coq/coq-syntax.el')
| -rw-r--r-- | coq/coq-syntax.el | 13 |
1 files changed, 11 insertions, 2 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 4bc8d984..5b12bd8e 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -1376,7 +1376,7 @@ part of another hypothesis.") (concat coq-hyp-name-in-goal-or-response-regexp "\\|\\(?1:^\\s-+========\\)") ) -(defun coq-detect-hyps-positions (buf) +(defun coq-detect-hyps-positions (buf &optional limit) "Detect all hypothesis displayed in buffer BUF and returns positions. 5 positions are created for each hyp: (begcross beghypname endhypname beg end)." @@ -1384,7 +1384,8 @@ endhypname beg end)." (save-excursion (goto-char (point-min)) (let ((res '())) - (while (search-forward-regexp coq-hyp-name-in-goal-or-response-regexp nil t) + (goto-char (point-min)) + (while (search-forward-regexp coq-hyp-name-in-goal-or-response-regexp limit t) (let* ((str (match-string 2)) (beghypname (match-beginning 2)) (beg (match-end 0)) @@ -1405,6 +1406,14 @@ endhypname beg end)." res)))) res)))) +;; Don't look at the conclusion of the goal +(defun coq-detect-hyps-positions-in-goals () + (with-current-buffer proof-goals-buffer + (goto-char (point-min)) + (coq-detect-hyps-positions + proof-goals-buffer + (if (search-forward-regexp "==========" nil t) (point) nil)))) + ;; We define a slightly different set of keywords for response buffer. |