Merge pull request #421 from jfehrle/for_master2

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

5 files changed, 27 insertions, 16 deletions

diff --git a/generic/pg-goals.el b/generic/pg-goals.el
index 37862a64..a76fbb44 100644
--- a/generic/pg-goals.el
+++ b/generic/pg-goals.el
@@ -25,6 +25,7 @@
 (defvar proof-assistant-menu)           ; defined by macro in proof-menu
 
 (require 'pg-assoc)
+(require 'coq-diffs)
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
@@ -109,7 +110,7 @@ so the response buffer should not be cleared."
 
     ;; Only display if string is non-empty.
     (unless (string-equal string "")
-      (insert string))
+      (coq-insert-tagged-text string))
 
     (setq buffer-read-only t)
     (set-buffer-modified-p nil)
diff --git a/generic/pg-response.el b/generic/pg-response.el
index 650e83a0..5fadca99 100644
--- a/generic/pg-response.el
+++ b/generic/pg-response.el
@@ -30,6 +30,7 @@
 
 (require 'pg-assoc)
 (require 'span)
+(require 'coq-diffs)
 
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -409,7 +410,9 @@ Returns non-nil if response buffer was cleared."
                     (eq (point-min) (point-max)))
           (newline))
         (setq start (point))
-        (insert str)
+        (if face
+          (insert str)
+          (coq-insert-tagged-text str))
         (unless (bolp) (newline))
         (when face
           (overlay-put
diff --git a/generic/proof-config.el b/generic/proof-config.el
index ea7fda8f..f9947757 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -213,9 +213,9 @@ Default is the identity function."
 (defcustom proof-assistant-setting-format nil
   "Function for formatting setting strings for proof assistant.
 Setting strings are calculated by replacing a format character
-%b, %i, or %s in the :setting string in for each variable defined with
-`defpacustom', using the current value of that variable.  This
-function  is applied as a final step to do any extra markup, or
+%b, %i, %f, %s, or %l in the :setting string in for each variable
+defined with `defpacustom', using the current value of that variable.
+This function is applied as a final step to do any extra markup, or
 conversion, etc.  (No changes are done if nil)."
   :type '(choice string (const nil))
   :group 'prover-config)
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index 2900a6b1..c17d4e95 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -860,6 +860,7 @@ KEY is the optional key binding."
 			 ["Save Settings" (proof-settings-save)
 			  (proof-settings-changed-from-saved-p)]))
 	    groups ents)
+	; todo: AFAICT the following statement does nothing and can be removed
 	(mapc (lambda (stg) (add-to-list 'groups (get (car stg) 'pggroup)))
 	      proof-assistant-settings)
 	(dolist (grp (reverse groups))
@@ -1004,7 +1005,8 @@ We first clear the dynamic settings from `proof-assistant-settings'."
    (cons "%b" '(proof-assistant-format-bool curvalue))
    (cons "%i" '(proof-assistant-format-int curvalue))
    (cons "%f" '(proof-assistant-format-float curvalue))
-   (cons "%s" '(proof-assistant-format-string curvalue)))
+   (cons "%s" '(proof-assistant-format-string curvalue))
+   (cons "%l" '(proof-assistant-format-lambda curvalue)))
   "Table to use with `proof-format' for formatting CURVALUE for assistant.
 NB: variable `curvalue' is dynamically scoped (used in `proof-assistant-format').")
 
@@ -1020,9 +1022,12 @@ NB: variable `curvalue' is dynamically scoped (used in `proof-assistant-format')
 (defun proof-assistant-format-string (value)
   (funcall proof-assistant-format-string-fn value))
 
+(defun proof-assistant-format-lambda (value)
+  (funcall value))
+
 (defun proof-assistant-format (string curvalue)
   "Replace a format characters in STRING by formatted CURVALUE.
-Format character is one of %b, %i, %f, or %s.
+Format character is one of %b, %i, %f, %s, or %l.
 Formatting suitable for current proof assistant, controlled by
 `proof-assistant-format-table' which see.
 Finally, apply `proof-assistant-setting-format' if non-nil.
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)