Merge pull request #421 from jfehrle/for_master2

Support Coq's proof diffs feature: highlight diffs in goals and some error messages

4 files changed, 159 insertions, 15 deletions

diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index a15db325..391b1238 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -124,7 +124,7 @@
     ["Double Hit Electric Terminator" coq-double-hit-toggle
      :style toggle
      :selected coq-double-hit-enable
-     :help "Automatically send commands when terminator typed twiced quickly."]
+     :help "Automatically send commands when terminator is typed twice quickly."]
     ("Auto Compilation"
      ["Compile Before Require"
       coq-compile-before-require-toggle
@@ -153,7 +153,7 @@
        :selected (eq coq-compile-quick 'no-quick)
        :active (and coq-compile-before-require
 		    coq-compile-parallel-in-background)
-       :help "Compile without -quick but accept existion .vio's"]
+       :help "Compile without -quick but accept existing .vio's"]
       ["quick no vio2vo"
        (customize-set-variable 'coq-compile-quick 'quick-no-vio2vo)
        :style radio
@@ -202,7 +202,7 @@
        :active coq-compile-before-require
        :help "Save all buffers without confirmation"]
       )
-     ["Lock Ancesotors"
+     ["Lock Ancestors"
       coq-lock-ancestors-toggle
       :style toggle
       :selected coq-lock-ancestors
@@ -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 662cc2e8..21b1acf9 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1216,7 +1216,8 @@ be called and no command will be sent to Coq."
           (> (length (coq-get-span-proofstack (proof-last-locked-span)))
              ;; the number of aborts is the third arg of Backtrack.
              (string-to-number (match-string 1 cmd)))))
-    (list "Unset Silent." "Show."))
+    ; "Set Diffs" always re-prints the proof context with (if enabled) diffs
+    (list "Unset Silent." (if (coq--post-v810) (coq-diffs) "Show.")))
    ((or
      ;; If we go back in the buffer and not in the above case, then only Unset
      ;; silent (there is no goal to show).
@@ -1225,7 +1226,7 @@ be called and no command will be sent to Coq."
 
 (defpacustom auto-adapt-printing-width t
   "If non-nil, adapt automatically printing width of goals window.
-Each timme the user sends abunch of commands to Coq, check if the
+Each time the user sends a bunch of commands to Coq, check if the
 width of the goals window changed, and adapt coq printing width.
 WARNING: If several windows are displaying the goals buffer, one
 is chosen arbitrarily.  WARNING 2: when backtracking the printing
@@ -1483,7 +1484,7 @@ fold/unfold cross.  Return the list of mappings hypname -> overlays."
   (cadr (assoc h coq-hyps-positions)))
 
 ;;;;;;;;;;;;;; Highlighting hypothesis ;;;;;;;;
-;; Feature: highlighting of hyptohesis that remains when the cript is played
+;; Feature: highlighting of hypothesis that remains when the script is played
 ;; (and goals buffer is updated).
 
 ;; On by default. This only works with the SearchAbout function for now.
@@ -1493,7 +1494,7 @@ fold/unfold cross.  Return the list of mappings hypname -> overlays."
 (defvar coq-highlight-hyps-sticky nil
   "If non-nil, try to make hypothesis highlighting sticky.
 The is try to re-highlight the hypothesis with same names
-after a refeshing of the response buffer.")
+after a refreshing of the response buffer.")
 
 ;; We maintain a list of hypothesis names that must be highlighted at each
 ;; regeneration of goals buffer.
@@ -1524,7 +1525,7 @@ buffer is updated."
 
 (defun coq-highlight-hyp (h)
   "Highlight hypothesis named H (sticky).
-use `coq-unhighlight-hyp' to unhilight."
+use `coq-unhighlight-hyp' to unhighlight."
   (unless (member h coq-highlighted-hyps)
     (setq coq-highlighted-hyps (cons h coq-highlighted-hyps)))
   (coq-highlight-hyp-aux h))
@@ -1768,7 +1769,14 @@ See  `coq-fold-hyp'."
 ;(proof-definvisible coq-set-printing-printing-depth "Set Printing Printing Depth . ")
 ;(proof-definvisible coq-unset-printing-printing-depth "Unset Printing Printing Depth . ")
 
-
+;; Persistent setting, non-boolean, non cross-version compatible (Coq >= 8.10)
+(defconst coq-diffs--function #'coq-diffs
+  "Symbol corresponding to the function `coq-diffs'.
+Required to benefit from delayed evaluation when
+`proof-assistant-format-lambda' calls (funcall coq-diffs--function)
+at `proof-assistant-settings-cmds' evaluation time.")
+(add-to-list 'proof-assistant-settings
+             '(diffs--function "%l" string "Show Diffs in Coq") t)
 
 (defun coq-Compile ()
   "Compiles current buffer."
@@ -1801,7 +1809,7 @@ See  `coq-fold-hyp'."
 ;; Set to t to bring it back%%
 ;;
 ;; FIXME: this always sets proof-output-tooltips to nil, even if the user puts
-;; explicitely the reverse in it sconfig file. I just want to change the
+;; explicitly the reverse in it sconfig file. I just want to change the
 ;; *default* value to nil.
 (custom-set-default 'proof-output-tooltips nil)
 
@@ -1891,7 +1899,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 +2078,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."
@@ -2230,7 +2266,7 @@ This is the Coq incarnation of `proof-tree-find-undo-position'."
 ;; after the proof, the evar line must be set back to what it was before the
 ;; proof. I therefore look in the urgent action hook if proof display is
 ;; switched on or off. When switched on, I test the current evar printing
-;; status with the undodumented command "Test Printing Dependent Evars Line" to
+;; status with the undocumented command "Test Printing Dependent Evars Line" to
 ;; remember if I have to switch evar printing off eventually.
 
 (defvar coq--proof-tree-must-disable-evars nil
@@ -2282,7 +2318,7 @@ properly after the proof and enable the evar printing."
   "Disable evar printing if necessary.
 This function switches off evar printing after the proof, if it
 was off before the proof.  For undo commands, we rely on the fact
-that Coq itself undos the effect of the evar printing change that
+that Coq itself undoes the effect of the evar printing change that
 we inserted after the goal statement.  We also rely on the fact
 that Proof General never backtracks into the middle of a
 proof.  (If this would happen, Coq would switch evar printing on
@@ -2299,7 +2335,7 @@ result of `coq-proof-tree-get-proof-info'."
 (defun coq-proof-tree-evar-display-toggle ()
   "Urgent action hook function for changing the evar printing status in Coq.
 This function is for `proof-tree-urgent-action-hook' (which is
-called only if external proof disaply is switched on).  It checks
+called only if external proof display is switched on).  It checks
 whether a proof was started or stopped and inserts commands for
 enableing and disabling the evar status line for Coq 8.6 or
 later.  Without the evar status line being enabled, prooftree
@@ -2779,7 +2815,7 @@ Completion is on a quasi-exhaustive list of Coq tacticals."
   "Last error from `coq-get-last-error-location' and `coq-highlight-error'.")
 
 
-;; I don't use proof-shell-last-ouput here since it is not always set to the
+;; I don't use proof-shell-last-output here since it is not always set to the
 ;; really last output (specially when a *tactic* gives an error) instead I go
 ;; directly to the response buffer. This allows also to clean the response
 ;; buffer (better to only scroll it?)