aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic
diff options
context:
space:
mode:
authorGravatar David Aspinall <da@inf.ed.ac.uk>2009-05-27 08:08:03 +0000
committerGravatar David Aspinall <da@inf.ed.ac.uk>2009-05-27 08:08:03 +0000
commite3016def0716977cb6a147c6b852e474eb1d69d1 (patch)
treeab23a91df94c4ae8aef8c7b2ea84831bfd59cec4 /generic
parentd5a8b652b307dddf844591d9a75e18a2fae9b253 (diff)
Check unicode-tokens-mode is bound
Diffstat (limited to 'generic')
-rw-r--r--generic/proof-script.el3
1 files changed, 2 insertions, 1 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el
index d4e91b62..1f554f39 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -702,7 +702,8 @@ NAME does not need to be unique."
"Add a daughter help span for SPAN with help message, highlight, actions"
(let ((helpmsg (pg-span-name span))
(proofstate (proof-shell-strip-output-markup
- (if unicode-tokens-mode
+ (if (and (boundp 'unicode-tokens-mode)
+ unicode-tokens-mode)
(unicode-tokens-encode-str proof-shell-last-output)
proof-shell-last-output)))
(newspan (let ((newstart (save-excursion