From 11dd30961fcd6c0f7e2d2ef48d4795961153d586 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Fri, 25 Sep 2009 22:18:14 +0000
Subject: pg-toggle-element-visibility: Add back `redraw-frame' call, it *is*
 needed here (possible Emacs bug)

---
 generic/proof-script.el | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

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."
-- 
cgit v1.2.3