Merge pull request #426 from jfehrle/tweak

Proof diffs revisions requested by @monnier

2 files changed, 54 insertions, 39 deletions

diff --git a/coq/coq-diffs.el b/coq/coq-diffs.el
index 7d5e8f58..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.
@@ -29,41 +32,50 @@ 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."
-  (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))
-      ;; 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))
-                 (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)
+;; 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
-                (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 21b1acf9..141bcb75 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -58,6 +58,8 @@
 (require 'coq-abbrev)                   ; abbrev and coq specific menu
 (require 'coq-seq-compile)              ; sequential compilation of Requires
 (require 'coq-par-compile)              ; parallel compilation of Requires
+(require 'coq-diffs)                    ; highlight proof diffs
+
 (defvar prettify-symbols-alist)
 
 
@@ -2081,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))
     ""))