diff options
| author | Pierre Courtieu | 2019-05-23 09:40:01 +0200 |
|---|---|---|
| committer | GitHub | 2019-05-23 09:40:01 +0200 |
| commit | 0058999ac42d7d1b3ee093aa5a4e8956d1eb8a9c (patch) | |
| tree | a24fc4fa9efd548355945b6595ec4d79fa7373cd /generic/proof-syntax.el | |
| parent | 5bdff05885b29be35962fb06b0339cdd34db1079 (diff) | |
| parent | 7501326a228a5d0af1ad1d5bef4e8640cbd1e43f (diff) | |
Merge pull request #421 from jfehrle/for_master2
Support Coq's proof diffs feature: highlight diffs in goals and some error messages
Diffstat (limited to 'generic/proof-syntax.el')
| -rw-r--r-- | generic/proof-syntax.el | 20 |
1 files changed, 11 insertions, 9 deletions
diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el index cdc38775..6fbe8eb0 100644 --- a/generic/proof-syntax.el +++ b/generic/proof-syntax.el @@ -244,15 +244,17 @@ may be a string or sexp evaluated to get a string." (while alist (let ((idx 0)) (while (string-match (car (car alist)) string idx) - (setq string - (concat (substring string 0 (match-beginning 0)) - (cond - ((stringp (cdr (car alist))) - (cdr (car alist))) - (t - (eval (cdr (car alist))))) - (substring string (match-end 0)))) - (setq idx (+ (match-beginning 0) (length (cdr (car alist))))))) + (let ((replacement + (cond + ((stringp (cdr (car alist))) + (cdr (car alist))) + (t + (eval (cdr (car alist))))))) + (setq string + (concat (substring string 0 (match-beginning 0)) + replacement + (substring string (match-end 0)))) + (setq idx (+ (match-beginning 0) (length replacement)))))) (setq alist (cdr alist))) string) |