diff options
| author | Makarius Wenzel | 2001-01-11 19:57:52 +0000 |
|---|---|---|
| committer | Makarius Wenzel | 2001-01-11 19:57:52 +0000 |
| commit | 742fe586cf81bde132d0389f70c5c459eb144860 (patch) | |
| tree | 909585f70c6ba16e4826e01cb9bf0d1131625a60 /generic/proof-script.el | |
| parent | a054106b5c0d6fed882fc6cfef55468205557277 (diff) | |
fixed format strings in message, error, etc.
Diffstat (limited to 'generic/proof-script.el')
| -rw-r--r-- | generic/proof-script.el | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index d25e83f5..938fb73b 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1124,7 +1124,7 @@ the ACS is marked in the current buffer. If CMD does not match any, (let (nam gspan next) ;; Try to set the name of the theorem from the save - (message cmd) + (message "%s" cmd) (and proof-save-with-hole-regexp (proof-string-match proof-save-with-hole-regexp cmd) @@ -1132,7 +1132,7 @@ the ACS is marked in the current buffer. If CMD does not match any, (if (stringp proof-save-with-hole-result) (replace-match proof-save-with-hole-result nil nil cmd) (match-string proof-save-with-hole-result cmd)))) - (message nam) + (message "%s" nam) ;; Search backwards for first goal command, ;; deleting spans along the way. (setq gspan span) @@ -1151,7 +1151,7 @@ the ACS is marked in the current buffer. If CMD does not match any, ;; If the name isn't set, try to set it from the goal. (unless nam (let ((cmdstr (span-property gspan 'cmd))) - (message cmdstr) + (message "%s" cmdstr) (and proof-goal-with-hole-regexp (proof-string-match proof-goal-with-hole-regexp cmdstr) (setq nam @@ -1295,7 +1295,7 @@ the ACS is marked in the current buffer. If CMD does not match any, ;; Try to set a name from the goal ;; (useless for provers like Isabelle) (let ((cmdstr (span-property gspan 'cmd))) - (message cmdstr) + (message "%s" cmdstr) (and proof-goal-with-hole-regexp (proof-string-match proof-goal-with-hole-regexp cmdstr) (setq nam |