diff options
| author | David Aspinall | 2003-10-05 15:55:12 +0000 |
|---|---|---|
| committer | David Aspinall | 2003-10-05 15:55:12 +0000 |
| commit | d0e4aa049840658bc5ed900511f46e7d2d45619d (patch) | |
| tree | c5b615dd38b933680a089df32d39aaa8e4a7ad8e /generic/proof-script.el | |
| parent | 9fd42ff8e8e5ddb3a1f26501f0bf1a9e54036ccc (diff) | |
Add interactive input setting, and extra flags for action.
Diffstat (limited to 'generic/proof-script.el')
| -rw-r--r-- | generic/proof-script.el | 6 |
1 files changed, 3 insertions, 3 deletions
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)))) |