From 0afe38adf55608b26f04a77f312d4805ce568da6 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Fri, 31 May 2019 16:59:19 -0700
Subject: Add hook for coq diff-highlighting routine
---
coq/coq-diffs.el | 12 ++++++++----
coq/coq.el | 5 +++++
generic/pg-goals.el | 8 +-------
generic/pg-response.el | 9 +++------
4 files changed, 17 insertions(+), 17 deletions(-)
mode change 100644 => 100755 generic/pg-goals.el
diff --git a/coq/coq-diffs.el b/coq/coq-diffs.el
index 7d5e8f58..67d2fcc7 100644
--- a/coq/coq-diffs.el
+++ b/coq/coq-diffs.el
@@ -29,6 +29,14 @@ For example 'foo' 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 "" are
+;; shown as-is. The user can turn off diffs in this very unlikely case.
+
(let* ((len (length str))
(off 0)
(fstack)
@@ -38,17 +46,13 @@ and applies the appropriate face.
(while (< off len)
(string-match "^\\([ \t]*\\)\\(.*\n?\\)" str off)
(setq off (match-end 0))
- ;; FIXME: Why handle whitespace specially?
(insert (match-string 1 str)) ;; begin-line white space
(setq rhs (match-string 2 str))
- ;; FIXME: Why handle whitespace specially?
(string-match "[ \t\n]*\\'" rhs)
(let* ((end-white (match-string 0 rhs)) ;; end-line white space
(line (substring rhs 0 (- (length rhs) (length end-white))))
(llen (length line))
(loff 0))
- ;; FIXME: I don't see any mechanism here to escape text, in case
- ;; we need to include text that happen to look just like a tag!
(while (and (< loff llen)
(string-match "<\\(/\\)?\\([a-zA-Z\\.]+\\)>" line loff))
(let* ((end-mark (match-beginning 1))
diff --git a/coq/coq.el b/coq/coq.el
index 21b1acf9..0f6d6f84 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -58,6 +58,11 @@
(require 'coq-abbrev) ; abbrev and coq specific menu
(require 'coq-seq-compile) ; sequential compilation of Requires
(require 'coq-par-compile) ; parallel compilation of Requires
+
+;; set hook for diff highlighting routine from non-Coq code
+(require 'coq-diffs)
+(setq pg-insert-text-function 'coq-insert-tagged-text)
+
(defvar prettify-symbols-alist)
diff --git a/generic/pg-goals.el b/generic/pg-goals.el
old mode 100644
new mode 100755
index 2474c402..d0897fbe
--- a/generic/pg-goals.el
+++ b/generic/pg-goals.el
@@ -26,12 +26,6 @@
(require 'pg-assoc)
-;; FIXME: This is required for `coq-insert-tagged-text', but we should never
-;; use Coq-specific code from a generic/*.el file. Actually, this `require'
-;; should fail if we're using PG with something else than Coq because the
-;; coq/ subdir won't be in `load-path'!
-(require 'coq-diffs)
-
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
;; Goals buffer mode
@@ -114,7 +108,7 @@ so the response buffer should not be cleared."
;; Only display if string is non-empty.
(unless (string-equal string "")
- (coq-insert-tagged-text string))
+ (funcall pg-insert-text-function string))
(setq buffer-read-only t)
(set-buffer-modified-p nil)
diff --git a/generic/pg-response.el b/generic/pg-response.el
index e94e710b..7f36fc6f 100644
--- a/generic/pg-response.el
+++ b/generic/pg-response.el
@@ -31,11 +31,8 @@
(require 'pg-assoc)
(require 'span)
-;; FIXME: This is required for `coq-insert-tagged-text', but we should never
-;; use Coq-specific code from a generic/*.el file. Actually, this `require'
-;; should fail if we're using PG with something else than Coq because the
-;; coq/ subdir won't be in `load-path'!
-(require 'coq-diffs)
+;; hook for coq diffs highlighting routine
+(defvar pg-insert-text-function 'insert)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -415,7 +412,7 @@ Returns non-nil if response buffer was cleared."
(let ((start (point)))
(if face
(insert str)
- (coq-insert-tagged-text str))
+ (funcall pg-insert-text-function str))
(unless (bolp) (newline))
(when face
;; FIXME: Why not (put-text-property start (point) 'face face)?
--
cgit v1.2.3
From 7f1821cee8801a0f248aef492b9c1541e85a4880 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Sat, 1 Jun 2019 01:43:09 -0700
Subject: Process tags in the buffer rather than in strings
---
coq/coq-diffs.el | 78 ++++++++++++++++++++++++++++----------------------
coq/coq.el | 6 ++--
generic/pg-response.el | 4 +--
3 files changed, 47 insertions(+), 41 deletions(-)
diff --git a/coq/coq-diffs.el b/coq/coq-diffs.el
index 67d2fcc7..ff71634a 100644
--- a/coq/coq-diffs.el
+++ b/coq/coq-diffs.el
@@ -15,12 +15,15 @@
;;; Code:
-(defun coq-insert-with-face (str face)
- (let ((start (point)))
- (insert str)
- (if face
- ;; FIXME: Why not (put-text-property start (point) 'face face)?
- (overlay-put (span-make start (point)) 'face face))))
+(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.
@@ -37,37 +40,42 @@ and applies the appropriate face.
;; that looks like a tag. Unknown tags such as "" are
;; shown as-is. The user can turn off diffs in this very unlikely case.
- (let* ((len (length str))
- (off 0)
- (fstack)
- (rhs))
- ;; FIXME: It would likely be better to insert `str' into the buffer
- ;; and then work in the buffer instead of manipulating strings.
- (while (< off len)
- (string-match "^\\([ \t]*\\)\\(.*\n?\\)" str off)
- (setq off (match-end 0))
- (insert (match-string 1 str)) ;; begin-line white space
- (setq rhs (match-string 2 str))
- (string-match "[ \t\n]*\\'" rhs)
- (let* ((end-white (match-string 0 rhs)) ;; end-line white space
- (line (substring rhs 0 (- (length rhs) (length end-white))))
- (llen (length line))
- (loff 0))
- (while (and (< loff llen)
- (string-match "<\\(/\\)?\\([a-zA-Z\\.]+\\)>" line loff))
- (let* ((end-mark (match-beginning 1))
- (tag (match-string 2 line))
- (face (cdr (assoc tag coq-tag-map)))
- (start (match-beginning 0))
- (end (match-end 0)))
- (coq-insert-with-face (substring line loff start) (car fstack))
- (setq loff end)
+ (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
- (setq fstack (if end-mark (cdr fstack) (cons face fstack)))
+ (progn
+ (replace-match "")
+ (setq fstack (if close-tag (cdr fstack) (cons face fstack))))
;; Unknown tag, show as-is!
- (coq-insert-with-face (substring line start end) (car fstack)))))
- (coq-insert-with-face (substring line loff) (car fstack))
- (insert end-white))))) ; end-line white space
+ (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)
diff --git a/coq/coq.el b/coq/coq.el
index 0f6d6f84..141bcb75 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -58,10 +58,7 @@
(require 'coq-abbrev) ; abbrev and coq specific menu
(require 'coq-seq-compile) ; sequential compilation of Requires
(require 'coq-par-compile) ; parallel compilation of Requires
-
-;; set hook for diff highlighting routine from non-Coq code
-(require 'coq-diffs)
-(setq pg-insert-text-function 'coq-insert-tagged-text)
+(require 'coq-diffs) ; highlight proof diffs
(defvar prettify-symbols-alist)
@@ -2086,6 +2083,7 @@ at `proof-assistant-settings-cmds' evaluation time.")
(defun coq-diffs ()
"Return string for setting Coq Diffs.
Return the empty string if the version of Coq < 8.10."
+ (setq pg-insert-text-function #'coq-insert-tagged-text)
(if (coq--post-v810)
(format "Set Diffs \"%s\". " (symbol-name coq-diffs))
""))
diff --git a/generic/pg-response.el b/generic/pg-response.el
index 7f36fc6f..37f629af 100644
--- a/generic/pg-response.el
+++ b/generic/pg-response.el
@@ -31,8 +31,8 @@
(require 'pg-assoc)
(require 'span)
-;; hook for coq diffs highlighting routine
-(defvar pg-insert-text-function 'insert)
+(defvar pg-insert-text-function #'insert
+ "hook for coq diffs highlighting routine")
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
--
cgit v1.2.3