From adcd209ec76e6899c98518766f88f4e18a669cbe Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 16 Sep 2009 09:25:59 +0000
Subject: pg-last-output-displayform: protect against empty string

---
 generic/proof-script.el | 23 ++++++++++++-----------
 1 file changed, 12 insertions(+), 11 deletions(-)

(limited to 'generic/proof-script.el')

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)
-- 
cgit v1.2.3