diff options
| author |  Makarius Wenzel <makarius@sketis.net> | 2000-12-06 19:11:23 +0000 |
|---|---|---|
| committer | Makarius Wenzel <makarius@sketis.net> | 2000-12-06 19:11:23 +0000 |
| commit | 6e6cec17adf7fa4f7235443a0480316f87bac72f (patch) | |
| tree | 90041653665ea2432528450233e88d1561d94738 /generic | |
| parent | 2d5763b803e0cb4110919951c141bd77f24d9a99 (diff) | |
fixed format strings for (message ...);
Diffstat (limited to 'generic')
| -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 fa1f4d0e..1e2c50aa 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1004,7 +1004,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) @@ -1012,7 +1012,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) @@ -1031,7 +1031,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 @@ -1165,7 +1165,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 |