diff options
| -rw-r--r-- | CHANGES | 8 | ||||
| -rw-r--r-- | coq/coq-abbrev.el | 22 | ||||
| -rw-r--r-- | coq/coq-db.el | 27 | ||||
| -rw-r--r-- | coq/coq-diffs.el | 65 | ||||
| -rw-r--r-- | coq/coq.el | 60 | ||||
| -rw-r--r-- | doc/ProofGeneral.texi | 66 | ||||
| -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 |
11 files changed, 244 insertions, 47 deletions
@@ -75,7 +75,6 @@ and the PG Trac http://proofgeneral.inf.ed.ac.uk/trac Hide/ unhide status remains when goal changes. - *** Highlighting of hypothesis You can highlight hypothesis in goals buffer on a per name @@ -84,8 +83,7 @@ and the PG Trac http://proofgeneral.inf.ed.ac.uk/trac Highlighting status remains when goal changes. - -**** Automtic highlighting with (search)About. +**** Automatic highlighting with (search)About. Hypothesis cited in the response buffer after C-c C-a C-a (i.e. M-x coq-SearchAbout) will be highlighted automatically. Any other hypothesis highlighted is unhighlighted. @@ -94,6 +92,10 @@ and the PG Trac http://proofgeneral.inf.ed.ac.uk/trac (setq coq-highlight-hyps-cited-in-response nil) +*** Support Coq's feature for highlighting the differences + between successive proof steps. See section 11.8 ("Showing + Proof Diffs") in the documentation. + *** bug fixes - avoid leaving partial files behind when compilation fails - 123: Parallel background compliation fails to execute some 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 @@ -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?) diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 56b9bbc6..ec449cc0 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -455,7 +455,7 @@ proof script@footnote{A @dfn{proof script} is a sequence of commands which constructs a proof, usually stored in a file.} in-place rather than line-by-line and later reassembling the pieces. Proof General keeps track of which proof steps have been processed by -the prover, and prevents you editing them accidently. You can undo +the prover, and prevents you editing them accidentally. You can undo steps as usual. The aim of Proof General is to provide a powerful and configurable @@ -465,7 +465,7 @@ should be useful for large proof developments. Please help us! -Send us comments, suggestsions, or (the best) patches to improve support +Send us comments, suggestions, or (the best) patches to improve support for your chosen proof assistant. Contact us at @uref{https://github.com/ProofGeneral/PG/issues}. @@ -931,7 +931,7 @@ is, you can find the option anyway on the menu: which also shows the key binding. If you want to use electric terminator, you can customize Proof -General to enable it everytime if you want, @xref{Customizing Proof +General to enable it every time if you want, @xref{Customizing Proof General}. For the common options, customization is easy: just use the menu item @code{Proof General -> Quick Options} to make your choices, and @code{Proof-General -> Quick Options -> Save Options} to @@ -1614,7 +1614,7 @@ key-bindings and functions. @c TEXI DOCSTRING MAGIC: proof-display-some-buffers @deffn Command proof-display-some-buffers -Display the reponse, trace, goals, or shell buffer, rotating.@* +Display the response, trace, goals, or shell buffer, rotating.@* A fixed number of repetitions of this command switches back to the same buffer. Also move point to the end of the response buffer if it's selected. @@ -1914,7 +1914,7 @@ an error, you might want to see that. You can select @lisp Proof-General -> Quick Options -> Display -> Sticky Errors @end lisp -to add a higlight for regions which did not successfully process +to add a highlight for regions which did not successfully process on the last attempt. Whenever the region is edited, the highlight is removed. @@ -2005,7 +2005,7 @@ interactive command processed some text (i.e., wasn't an undo step backwards into the buffer) and processing didn't stop with an error. To start automatic processing again after an error, simply hit @kbd{C-c C-n} after editing the buffer. To turn the automatic processing on or -off from the keyboard, you can use the keybinding: +off from the keyboard, you can use the key binding: @table @kbd @item C-c > @@ -3452,7 +3452,7 @@ buffers or refresh the window layout. These are on the menu: @c TEXI DOCSTRING MAGIC: proof-display-some-buffers @deffn Command proof-display-some-buffers -Display the reponse, trace, goals, or shell buffer, rotating.@* +Display the response, trace, goals, or shell buffer, rotating.@* A fixed number of repetitions of this command switches back to the same buffer. Also move point to the end of the response buffer if it's selected. @@ -4302,6 +4302,7 @@ assistant. It supports most of the generic features of Proof General. * User-loaded tactics:: * Holes feature:: * Proof-Tree Visualization:: +* Showing Proof Diffs:: @end menu @@ -4427,13 +4428,13 @@ Documentation of the user option @code{coq-project-filename}: @c TEXI DOCSTRING MAGIC: coq-project-filename @defvar coq-project-filename The name of coq project file.@* -The coq project file of a coq developpement (Cf Coq documentation +The coq project file of a coq development (Cf Coq documentation on "makefile generation") should contain the arguments given to coq_makefile. In particular it contains the -I and -R options (preferably one per line). If @samp{coq-use-coqproject} is -t (default) the content of this file will be used by proofgeneral +t (default) the content of this file will be used by Proof General to infer the @samp{@code{coq-load-path}} and the @samp{@code{coq-prog-args}} variables -that set the coqtop invocation by proofgeneral. This is now the +that set the coqtop invocation by Proof General. This is now the recommended way of configuring the coqtop invocation. Local file variables may still be used to override the coq project file's configuration. .dir-locals.el files also work and override @@ -5077,7 +5078,7 @@ one. This is supported to any nesting depth that Coq allows. Warning! Using Coq commands for navigating inside the different proofs (@code{Resume} and especially @code{Suspend}) are not supported, -backtracking will break syncronization. +backtracking will break synchronization. @b{Special note:} The old feature that moved nested proofs outside the current proof is disabled. @@ -5190,6 +5191,45 @@ To support @code{Grab Existential Variables} Prooftree can actually display several graphically independent proof trees in several layers. +@node Showing Proof Diffs +@section Showing Proof Diffs + +Coq 8.10 supports automatically highlighting the differences +between successive proof steps in Proof General. The feature is described in the +@uref{https://coq.inria.fr/distrib/current/refman/proof-engine/proof-handling.html#showing-differences-between-proof-steps, +Coq Documentation}. + +The Coq proof diff does more than a basic "diff" operation. For example: + +@itemize @bullet +@item diffs are computed on a per-token basis (as determined by the Coq lexer) rather + than on a per-character basis, probably a better match for how people understand + the output. (For example, a token-based diff between "abc" and "axc" will + highlight all of "abc" and "axc" as a difference, while a character-based diff + would indicate that "a" and "c" are in common and that only the "b"/"x" is a + difference.) +@item diffs ignore the order of hypotheses +@item tactics that only change the proof view are handled specially, for + example "swap" after a "split" will show the diffs between before "split" + and after "swap", which is more useful +@item some error messages have been instrumented to show diffs where it is helpful +@end itemize + +To enable or disable diffs, set @code{coq-diffs} (select menu @code{Coq -> Diffs}) +to "on", "off" or "removed". "on" highlights added tokens with the background +color from @code{diff-refine-added}. "removed" highlights removed tokens +with the background color from @code{diff-refine-removed}. With the "removed" setting, +lines that have both added and removed text may be shown twice, as "before" and +"after" lines. +To preserve the settings for the next time you start Proof General, +select @code{Coq -> Settings -> Save Settings}. + +The colors used to highlight diffs are configurable in the +@code{Proof-General -> Advanced -> Customize -> Proof Faces} menu. +The 4 @code{Coq Diffs ...} faces control the highlights. Lines that +have added or removed tokens are shown with the entire line highlighted with +a @code{Coq Diffs ... Bg} face. The added or removed tokens themselves are highlighted +with non-@code{Bg} faces. @c ================================================================= @c @@ -5244,7 +5284,7 @@ keyboard command @code{isabelle-chose-logic} to choose from the list. The logics list is refreshed dynamically so you can select any newly built heap images in the same Emacs session. However, notice that the -choices are greyed out while Isabelle is actually runnning --- you can +choices are greyed out while Isabelle is actually running --- you can only switch to a new logic if you first exit Isabelle (similarly to Proof General, Isabelle operates with only one logic at a time). @@ -6139,7 +6179,7 @@ There was no 3.6 release of Proof General. Proof General version 3.7.1 is an updated and enhanced version of Proof General 3.7. See @file{CHANGES} for more details. -Proof General version 3.7 collects together a cummulative set of +Proof General version 3.7 collects together a cumulative set of improvements to Proof General 3.5. There are compatibility fixes for newer Emacs versions, and particularly for GNU Emacs: credit is due to Stefan Monnier for an intense period of debugging and patching. The 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) |