diff options
| -rw-r--r-- | generic/pg-xml.el | 36 | ||||
| -rw-r--r-- | generic/proof-script.el | 8 | ||||
| -rw-r--r-- | generic/proof-shell.el | 7 |
3 files changed, 21 insertions, 30 deletions
diff --git a/generic/pg-xml.el b/generic/pg-xml.el index 1df7e33e..75954108 100644 --- a/generic/pg-xml.el +++ b/generic/pg-xml.el @@ -102,10 +102,8 @@ is (setq attrs (reverse attrs)) ;; Now we ought to be at the end of the element opening (unless (looking-at pg-xml-end-open-elt-regexp) - (error - (format - "pg-xml-parse-buffer: Invalid XML in element opening %s" - (symbol-name elt)))) + (error "pg-xml-parse-buffer: Invalid XML in element opening %s" + (symbol-name elt))) ;; Stack the element unless it's self closing (if (> (length (match-string 1)) 0) ;; Add element without nesting @@ -124,13 +122,11 @@ is (setq elt (intern (match-string 1))) ;; It better be the top thing on the stack (unless (eq elt (car-safe openelts)) - (error - (format - "pg-xml-parse-buffer: Invalid XML at element closing </%s> (expected </%s>)" - (symbol-name elt) - (if openelts - (symbol-name (car openelts)) - "no closing element")))) + (error "pg-xml-parse-buffer: Invalid XML at element closing </%s> (expected </%s>)" + (symbol-name elt) + (if openelts + (symbol-name (car openelts)) + "no closing element"))) ;; Add text before here to the parse (pg-xml-add-text (buffer-substring pos (match-beginning 0))) ;; Unstack the element and close subtree @@ -145,23 +141,19 @@ is ;; CASE 3: comment ((looking-at pg-xml-comment-start-regexp) (unless (re-search-forward pg-xml-comment-end-regexp nil t) - (error - (format - "pg-xml-parse-buffer: Unclosed comment beginning at line %s" - (1+ (count-lines (point-min) (point))))))))) + (error "pg-xml-parse-buffer: Unclosed comment beginning at line %s" + (1+ (count-lines (point-min) (point)))))))) ;; We'd better have nothing on the stack of open elements now. (unless (null openelts) - (error - (format "pg-xml-parse-buffer: Unexpected end of document, expected </%s>" - (symbol-name (car openelts))))) + (error "pg-xml-parse-buffer: Unexpected end of document, expected </%s>" + (symbol-name (car openelts)))) ;; And we'd better be at the end of the document. (unless (and (looking-at "[ \t\n]*") (eq (match-end 0) (point-max))) - (warn - (format "pg-xml-parse-buffer: Junk at end of document: %s" - (buffer-substring (point) - (min (point-max) (+ 30 (point-max))))))) + (warn "pg-xml-parse-buffer: Junk at end of document: %s" + (buffer-substring (point) + (min (point-max) (+ 30 (point-max)))))) ;; Return the parse ;; FIXME: (caar xmlparse)))) 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 diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 73950cc2..d775d285 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -193,7 +193,7 @@ Does nothing if proof assistant is already running." ;; ugly (coqtop, hol.unquote). ((proc (downcase proof-assistant))) - (message (format "Starting process: %s" proof-prog-name)) + (message "Starting process: %s" proof-prog-name) ;; Starting the inferior process (asynchronous) (let ((prog-name-list @@ -226,7 +226,7 @@ Does nothing if proof assistant is already running." ;; exiting immediately. ;; Might still be problems here if sentinels are set. (setq proof-shell-buffer nil) - (error (format "Starting process: %s..failed" proof-prog-name))) + (error "Starting process: %s..failed" proof-prog-name)) ;; Create the associated buffers and set buffer variables (let ((goals (concat "*" proc "-goals*")) @@ -271,8 +271,7 @@ Does nothing if proof assistant is already running." (funcall proof-mode-for-goals)) (switch-to-buffer proof-shell-buffer) (error "%s process exited!" proc))) - (message - (format "Starting %s process... done." proc))))) + (message "Starting %s process... done." proc)))) ;; |