diff options
author | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2018-05-31 13:20:03 +0200 |
---|---|---|
committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2018-05-31 13:20:03 +0200 |
commit | f743d1280026575275aef95d0c3eceead81614b6 (patch) | |
tree | 26884b955a91e40bc461ae8c48fc1853decc35af /coq/coq-syntax.el | |
parent | 315b7043953449fd6d982b01e4bcda91bb37ae7e (diff) |
Infrastructure for transient hyps highlighting.
Diffstat (limited to 'coq/coq-syntax.el')
-rw-r--r-- | coq/coq-syntax.el | 24 |
1 files changed, 23 insertions, 1 deletions
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 63d44666..61bb9751 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -1358,9 +1358,31 @@ It is used: ;; 1 space this is a hypothesis displayed in the middle of a line (> v8.5) ;; "^ " is for goals in debug mode. (defvar coq-hyp-name-in-goal-or-response-regexp - "\\(^\\|^ \\|^ \\|[^^ ] ? \\)\\(\\(?:[^\n :(),=]\\|, \\)+ *\\(?::[ \n]\\|,$\\)\\)" + "\\(^\\|^ \\|^ \\|[^^ ] ? \\)\\(?:\\(?2:\\(?:[^\n :(),=]\\|, \\)+\\) *\\(?::[ \n]\\|,$\\)\\)" "regexp matching hypothesis names in goal or response buffer") +(defvar coq-hyp-name-or-goalsep-in-goal-or-response-regexp + (concat coq-hyp-name-in-goal-or-response-regexp "\\|\n\\s-+========") + ) + +(defun coq-detect-hyps (buf) + (with-current-buffer buf + (save-excursion + (goto-char (point-min)) + (let ((res '())) + (while (search-forward-regexp coq-hyp-name-in-goal-or-response-regexp nil t) + (let* ((str (match-string 2)) + (beg (match-beginning 2)) + (splitstr (split-string str ",\\|,$\\|:" t "\\s-")) + (end (save-excursion + (search-forward-regexp coq-hyp-name-or-goalsep-in-goal-or-response-regexp nil t) + (match-beginning 0)))) + (mapcar + (lambda (s) (setq res (cons (cons (substring-no-properties s) (cons beg (cons end nil))) res))) + splitstr))) + ;; TODO: register thje last hyp. + res)))) + ;; We define a slightly different set of keywords for response buffer. (defvar coq-response-font-lock-keywords |