diff options
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/pg-goals.el | 3 | ||||
| -rw-r--r-- | generic/pg-response.el | 5 | ||||
| -rw-r--r-- | generic/proof-config.el | 6 | ||||
| -rw-r--r-- | generic/proof-menu.el | 9 | ||||
| -rw-r--r-- | generic/proof-syntax.el | 20 |
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) |