diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2010-12-16 00:11:21 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2010-12-16 00:11:21 +0000 |
| commit | 66249f4ec219c140208e6c9415116a8c58476e28 (patch) | |
| tree | b68d0c0dad71c40a140221aa57822a3cc23f9847 /generic/proof-menu.el | |
| parent | 813d75c12f0624895ad9df8701ed72be1fca616b (diff) | |
Patch to add pgipfloat type.
Diffstat (limited to 'generic/proof-menu.el')
| -rw-r--r-- | generic/proof-menu.el | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/generic/proof-menu.el b/generic/proof-menu.el index 693a4ad2..1253a12a 100644 --- a/generic/proof-menu.el +++ b/generic/proof-menu.el @@ -947,6 +947,7 @@ KEY is the optional key binding." (list (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))) "Table to use with `proof-format' for formatting CURVALUE for assistant. NB: variable curvalue is dynamically scoped (used in `proof-assistant-format').") @@ -957,11 +958,15 @@ NB: variable curvalue is dynamically scoped (used in `proof-assistant-format')." (defun proof-assistant-format-int (value) (funcall proof-assistant-format-int-fn value)) +(defun proof-assistant-format-float (value) + (funcall proof-assistant-format-float-fn value)) + (defun proof-assistant-format-string (value) (funcall proof-assistant-format-string-fn value)) (defun proof-assistant-format (string curvalue) - "Replace a format characters %b %i %s in STRING by formatted CURVALUE. + "Replace a format characters in STRING by formatted CURVALUE. +Format character is one of %b, %i, %f, or %s. Formatting suitable for current proof assistant, controlled by `proof-assistant-format-table' which see. Finally, apply `proof-assistant-setting-format' if non-nil. |