Highlight diffs in goals and some error messages

using Coq's proof diffs feature.

4 files changed, 137 insertions, 1 deletions

diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index 4d2d2d0e..391b1238 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -220,6 +220,22 @@
       :active (and coq-compile-before-require
 		   coq-compile-parallel-in-background)
       :help "Abort background compilation and kill all compilation processes."])
+    ("Diffs"
+      ["off"
+       (customize-set-variable 'coq-diffs 'off)
+       :style radio
+       :selected (eq coq-diffs 'off)
+       :help "Don't show diffs"]
+      ["on"
+       (customize-set-variable 'coq-diffs 'on)
+       :style radio
+       :selected (eq coq-diffs 'on)
+       :help "Show diffs: only added"]
+      ["removed"
+       (customize-set-variable 'coq-diffs 'removed)
+       :style radio
+       :selected (eq coq-diffs 'removed)
+       :help "Show diffs: added and removed"])
     ""
     ["Print..." coq-Print :help "With prefix arg (C-u): Set Printing All first"]
     ["Check..." coq-Check :help "With prefix arg (C-u): Set Printing All first"]
diff --git a/coq/coq-db.el b/coq/coq-db.el
index b01e8018..758177c9 100644
--- a/coq/coq-db.el
+++ b/coq/coq-db.el
@@ -26,6 +26,7 @@
 (eval-when-compile (require 'cl-lib))   ;decf
 
 (require 'holes)
+(require 'diff-mode)
 
 (defconst coq-syntax-db nil
   "Documentation-only variable, for coq keyword databases.
@@ -365,6 +366,32 @@ Required so that 'coq-symbol-binder-face is a proper facename")
 (defconst coq-question-mark-face 'coq-question-mark-face)
 
 
+(defface coq-diffs-added-face
+  '((t . (:inherit diff-refine-added)))
+  "Face used to highlight added text in diffs"
+  :group 'proof-faces)
+
+(defface coq-diffs-removed-face
+  '((t . (:inherit diff-refine-removed)))
+  "Face used to highlight removed text in diffs"
+  :group 'proof-faces)
+
+(defface coq-diffs-added-bg-face
+  '((t . (:inherit diff-added)))
+  "Face used to highlight unchanged text in lines showing added text in diffs"
+  :group 'proof-faces)
+
+(defface coq-diffs-removed-bg-face
+  '((t . (:inherit diff-removed)))
+  "Face used to highlight unchanged text in lines showing removed text in diffs"
+  :group 'proof-faces)
+
+(defvar coq-tag-map
+  '(("diff.added" . coq-diffs-added-face)
+   ("diff.removed" . coq-diffs-removed-face)
+   ("diff.added.bg" . coq-diffs-added-bg-face)
+   ("diff.removed.bg" . coq-diffs-removed-bg-face)))
+
 (provide 'coq-db)
 
 ;;; coq-db.el ends here
diff --git a/coq/coq-diffs.el b/coq/coq-diffs.el
new file mode 100644
index 00000000..d93adf73
--- /dev/null
+++ b/coq/coq-diffs.el
@@ -0,0 +1,65 @@
+;;; 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-insert-with-face (str face)
+  (let ((start (point)))
+    (insert str)
+    (if face
+      (overlay-put (span-make start (point-max)) 'face face))))
+
+(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."
+  (let* ((len (length str))
+         (off 0)
+	     (fstack)
+	     (rhs))
+    (while (< off len)
+      (string-match "^\\([ \t]*\\)\\(.*\n?\\)" str off)
+      (setq off (match-end 0))
+      (coq-insert-with-face (match-string 1 str) nil)  ;; 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 (< loff llen)
+          (if (> loff 0)
+            (aset line (1- loff) ?\n))   ;; only way to get an anchored search midstring
+          (cond
+            ; make sure that a) the matched string is never the empty string, and
+            ; b) that every non-empty string has a match
+            ((string-match "^<\\(/?\\)\\([a-zA-Z\\.]+\\)>" line loff)    ;; tag
+              (let* ((end-mark (match-string 1 line))
+                     (tag (match-string 2 line))
+                     (face (cdr (assoc tag coq-tag-map))))
+                (if face
+                  (setq fstack (if (equal end-mark "") (cons face fstack) (cdr fstack)))
+                  (coq-insert-with-face (match-string 0 line) (car fstack)))))    ;; unknown tag, show as-is
+            ((string-match "^<?[^<\n]+" line loff)    ;; text
+              (coq-insert-with-face (match-string 0 line) (car fstack))))
+          (setq loff (match-end 0)))
+        (coq-insert-with-face end-white nil)))))    ; end-line white space
+
+(provide 'coq-diffs)
+
+;;; coq-diffs.el ends here
diff --git a/coq/coq.el b/coq/coq.el
index 3eb5f0cb..ed71b1b3 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1891,7 +1891,7 @@ See  `coq-fold-hyp'."
   ;; type.
   (setq proof-assistant-additional-settings
         '(coq-compile-quick coq-compile-keep-going
-          coq-compile-auto-save coq-lock-ancestors))
+          coq-compile-auto-save coq-lock-ancestors coq-diffs))
 
   (setq proof-goal-command-p #'coq-goal-command-p
         proof-find-and-forget-fn #'coq-find-and-forget
@@ -2070,6 +2070,34 @@ See  `coq-fold-hyp'."
   :type 'integer
   :setting "Set Printing Depth %i . ")
 
+(defun coq-diffs ()
+  "Return string for setting Coq Diffs.
+Return the empty string if the version of Coq < 8.10."
+  (if (coq--post-v810)
+      (format "Set Diffs \"%s\". " (symbol-name coq-diffs))
+    ""))
+
+(defun coq-diffs--setter (symbol new-value)
+  ":set function fo `coq-diffs'.
+Set Diffs setting if Coq is running and has a version >= 8.10."
+  (set symbol new-value)
+  (if (proof-shell-available-p)
+      (let ((cmd (coq-diffs)))
+        (if (equal cmd "")
+            (message "Ignore coq-diffs setting %s for Coq before 8.10"
+                 (symbol-name coq-diffs))
+          (proof-shell-invisible-command cmd)))))
+
+(defcustom coq-diffs 'off
+  "Controls Coq Diffs option"
+  :type '(radio
+    (const :tag "Don't show diffs" off)
+    (const :tag "Show diffs: only added" on)
+    (const :tag "Show diffs: added and removed" removed))
+  :safe (lambda (v) (member v '(off on removed)))
+  :set 'coq-diffs--setter
+  :group 'coq)
+
 ;; Obsolete:
 ;;(defpacustom undo-depth coq-default-undo-limit
 ;;  "Depth of undo history.  Undo behaviour will break beyond this size."