From d0e4aa049840658bc5ed900511f46e7d2d45619d Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Sun, 5 Oct 2003 15:55:12 +0000 Subject: Add interactive input setting, and extra flags for action. --- generic/proof-script.el | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'generic/proof-script.el') diff --git a/generic/proof-script.el b/generic/proof-script.el index 8e65298d..222bb69d 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -690,7 +690,7 @@ NAME does not need to be unique." (defun pg-set-span-helphighlights (span &optional nohighlight) "Set the help echo message, default highlight, and keymap for SPAN." - (let ((helpmsg (concat (pg-span-name span) " region"))) + (let ((helpmsg (concat (pg-span-name span) ""))) ;; " region" (set-span-property span 'balloon-help helpmsg) (if pg-show-hints ;; only message in minibuf if hints on (set-span-property @@ -700,8 +700,8 @@ NAME does not need to be unique." helpmsg " (" (if (span-property span 'idiom) - "with point in region, use \\[pg-toggle-visibility] to show/hide; ") - "use \\[popup-mode-menu] for menu)")))) + "with point in region, \\[pg-toggle-visibility] to show/hide; ") + "\\[popup-mode-menu] for menu)")))) (set-span-property span 'keymap pg-span-context-menu-keymap) (unless nohighlight (set-span-property span 'mouse-face 'proof-mouse-highlight-face)))) -- cgit v1.2.3