diff options
| author | David Aspinall | 2009-09-16 09:25:59 +0000 |
|---|---|---|
| committer | David Aspinall | 2009-09-16 09:25:59 +0000 |
| commit | adcd209ec76e6899c98518766f88f4e18a669cbe (patch) | |
| tree | 5f0c77bcfbe6538b1362dc368bb63c52462d0352 /generic/proof-script.el | |
| parent | b1472fb627a847b610ff82a2ebdf85241576169b (diff) | |
pg-last-output-displayform: protect against empty string
Diffstat (limited to 'generic/proof-script.el')
| -rw-r--r-- | generic/proof-script.el | 23 |
1 files changed, 12 insertions, 11 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index 9ba6b46f..fac7c642 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -643,17 +643,18 @@ NAME does not need to be unique." (defun pg-last-output-displayform () "Return displayable form of `proof-shell-last-output'." - (let ((text (proof-shell-strip-output-markup - (if (and (boundp 'unicode-tokens-mode) - unicode-tokens-mode) - (unicode-tokens-encode-str proof-shell-last-output) - proof-shell-last-output)))) - ;; NOTE: hack for Isabelle which puts ugly leading \n's around proofstate. - (if (string= (substring text 0 1) "\n") - (setq text (substring text 1))) - (if (string= (substring text -1) "\n") - (setq text (substring text 0 -1))) - text)) + (if (string= proof-shell-last-output "") "" + (let ((text (proof-shell-strip-output-markup + (if (and (boundp 'unicode-tokens-mode) + unicode-tokens-mode) + (unicode-tokens-encode-str proof-shell-last-output) + proof-shell-last-output)))) + ;; NOTE: hack for Isabelle which puts ugly leading \n's around proofstate. + (if (string= (substring text 0 1) "\n") + (setq text (substring text 1))) + (if (string= (substring text -1) "\n") + (setq text (substring text 0 -1))) + text))) ;;;###autoload (defun pg-set-span-helphighlights (span &optional mouseface face) |