diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2009-09-25 22:18:14 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2009-09-25 22:18:14 +0000 |
| commit | 11dd30961fcd6c0f7e2d2ef48d4795961153d586 (patch) | |
| tree | 4521ba7f62e4bdaef3cefa384d1c058b5d963c43 /generic/proof-script.el | |
| parent | f3adf335e01ad89818a3edfa643defbdf28d46cd (diff) | |
pg-toggle-element-visibility: Add back `redraw-frame' call, it *is*
needed here (possible Emacs bug)
Diffstat (limited to 'generic/proof-script.el')
| -rw-r--r-- | generic/proof-script.el | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index 50a718bb..9438abc3 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -567,9 +567,13 @@ NAME does not need to be unique." (defun pg-toggle-element-visibility (idiom id) "Toggle visibility of script element of type IDIOM, named ID." + (interactive) (if (assq (pg-visname idiom id) buffer-invisibility-spec) (pg-make-element-visible idiom id) - (pg-make-element-invisible idiom id))) + (pg-make-element-invisible idiom id)) + ;; GNU Emacs sometimes requires redisplay for change + ;; in `buffer-invisibility-spec', perhaps a bug? + (redraw-frame (selected-frame))) (defun pg-show-all-portions (idiom &optional hide) "Show or conceal portions of kind IDIOM; if HIDE is non-nil, conceal." |