From 5a855bb5075574763d02248e57bd705643be84f1 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Fri, 14 Aug 2009 12:53:54 +0000 Subject: pg-last-output-displayform: add convenience function --- generic/proof-script.el | 24 +++++++++++++++--------- 1 file changed, 15 insertions(+), 9 deletions(-) (limited to 'generic/proof-script.el') diff --git a/generic/proof-script.el b/generic/proof-script.el index 00e3c5a7..3ff1aa34 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -722,23 +722,29 @@ NAME does not need to be unique." map) "Keymap for the span context menu.") +(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 in proofstate. + (if (eq (string-match "^\n" text) 0) + (setq text (substring text 1))) + text)) + ;;;###autoload (defun pg-set-span-helphighlights (span &optional nohighlight) - "Add a daughter help span for SPAN with help message, highlight, actions" + "Add a daughter help span for SPAN with help message, highlight, actions. +We add the last output to the hover display here." (let ((helpmsg (pg-span-name span)) - (proofstate (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))) + (proofstate (pg-last-output-displayform)) (newspan (let ((newstart (save-excursion (goto-char (span-start span)) (skip-chars-forward " \n\t") (point)))) (span-make newstart (span-end span))))) - ;; NOTE: hack for Isabelle which puts ugly leading \n's in proofstate. - (if (eq (string-match "^\n" proofstate) 0) - (setq proofstate (substring proofstate 1))) (setq helpmsg (concat (if (> (length proofstate) 2) "" helpmsg) proofstate)) -- cgit v1.2.3