blob: ff71634aa5854484be4b755d629512ce71b1a3d5 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
|
;;; coq-diffs.el --- highlight text marked with XML-like tags for Coq diffs
;; This file is part of Proof General.
;; Portions © Copyright 2019 Jim Fehrle
;; Author: Jim Fehrle <jim.fehrle@gmail.com>
;; License: BSD-3 (3-Clause BSD License)
;;; Commentary:
;;
(require 'coq-db)
;;; Code:
(defun coq-highlight-with-face (end face)
(if face
;; (put-text-property (point) end 'face face) doesn't work
(overlay-put (span-make (point) end) 'face face))
(goto-char end))
(defun coq-search (regex limit)
(save-excursion
(re-search-forward regex limit t)))
(defun coq-insert-tagged-text (str)
"Insert text into the current buffer applying faces specified by tags.
For example '<diff.added>foo</diff.added>' inserts 'foo' in the buffer
and applies the appropriate face.
`coq-tag-map' defines the mapping from tag name to face."
;; Coq inserts tags before splitting into lines. Avoid highlighting
;; white space at the beginning or end of lines in a conclusion or
;; hypothesis that's split across multiple lines.
;; Doesn't handle the unlikely case of escaping regular text
;; that looks like a tag. Unknown tags such as "<foo>" are
;; shown as-is. The user can turn off diffs in this very unlikely case.
(let* ((fstack)
(start (point))
(strend)
(lend)
(end-white-begin))
(insert str)
(setq strend (copy-marker (point)))
(goto-char start)
(while (< (point) strend)
(coq-search "^\\([ \t]*\\).*\\(\n\\)?" strend)
(setq lend (copy-marker (match-end 0)))
(if (match-end 1)
(goto-char (match-end 1))) ;; begin-line white space
(let* ((nl (if (match-string 2) 1 0))
(end-white-len ;; length of end-line white space
(if (coq-search "[ \t\n]*\\'" lend)
(- (match-end 0) (match-beginning 0))
0)))
(setq end-white-begin (copy-marker (- (- lend end-white-len) nl)))
(while (and (< (point) lend)
(coq-search "<\\(/\\)?\\([a-zA-Z\\.]+\\)>" lend))
(let* ((close-tag (match-beginning 1))
(tag (match-string 2))
(face (cdr (assoc tag coq-tag-map)))
(start (match-beginning 0))
(end (match-end 0)))
(coq-highlight-with-face start (car fstack)) ;; text before tag
(if face
(progn
(replace-match "")
(setq fstack (if close-tag (cdr fstack) (cons face fstack))))
;; Unknown tag, show as-is!
(coq-highlight-with-face end (car fstack)))))
(coq-highlight-with-face end-white-begin (car fstack)) ;; text after last tag
(goto-char lend))))) ;; end-line white space
(provide 'coq-diffs)
;;; coq-diffs.el ends here
|
