diff options
| -rw-r--r-- | generic/pg-pgip.el | 7 | ||||
| -rw-r--r-- | generic/proof-config.el | 7 | ||||
| -rw-r--r-- | generic/proof-menu.el | 7 |
3 files changed, 18 insertions, 3 deletions
diff --git a/generic/pg-pgip.el b/generic/pg-pgip.el index 6c736fae..16a0a6bd 100644 --- a/generic/pg-pgip.el +++ b/generic/pg-pgip.el @@ -466,6 +466,7 @@ Also sets local proverid and srcid variables for buffer." (cond ((eq tyname 'pgipbool) 'boolean) ((eq tyname 'pgipint) 'integer) ;; TODO: implement range limits + ((eq tyname 'pgipfloat) 'float) ;; TODO: implement range limits ((eq tyname 'pgipstring) 'string) ((eq tyname 'pgipconst) (let ((name (pg-pgip-get-name node 'optional)) @@ -498,6 +499,7 @@ Also sets local proverid and srcid variables for buffer." (cond ((eq type 'boolean) "%b") ((eq type 'integer) "%i") + ((eq type 'float) "%f") (t "%s"))) @@ -515,8 +517,9 @@ Also sets local proverid and srcid variables for buffer." (t (progn (pg-pgip-warning "pg-pgip-interpret-value: received non-bool value %s" value) nil)))) - ((eq type 'integer) (string-to-number value)) - ((eq type 'string) value) + ((eq type 'integer) (string-to-number value)) + ((eq type 'float) (string-to-number value)) + ((eq type 'string) value) ((eq (car-safe type) 'const) value) ((eq (car-safe type) 'choice) (pg-pgip-interpret-choice (cdr type) value)) diff --git a/generic/proof-config.el b/generic/proof-config.el index 0ede4c5f..cd41084a 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -189,6 +189,13 @@ Default is `int-to-string'." :type 'function :group 'prover-config) +(defcustom proof-assistant-format-float-fn 'number-to-string + "Function for converting float values to ints in proof assistant. +Used for configuring settings in proof assistant. +Default is `number-to-string'." + :type 'function + :group 'prover-config) + (defcustom proof-assistant-format-string-fn (lambda (value) value) "Function for converting string values to strings in proof assistant. Used for configuring settings in proof assistant. 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. |