Multiple frames annoyances, also proof-eagerly-raise setting.

1 files changed, 30 insertions, 0 deletions

diff --git a/BUGS b/BUGS
index a39f5a7b..d062549f 100644
--- a/BUGS
+++ b/BUGS
@@ -38,6 +38,36 @@ simplifier, when tracing rewriting.  It seems to be worse on
 certain architectures, and slower machines.  Behaviour seems
 better on Emacs than XEmacs.
 
+** Glitches in display handling, esp with multiple frames
+
+Unfortunately the handling of the display is very difficult to manage
+because the API provided by Emacs is quirky, buggy, and varies between
+versions.  If the eager display/tear-down of frames is annoying you,
+you may customize the variable `proof-shell-fiddle-frames' to nil to
+reduce it a bit.  To prevent eagerly displaying new frames at on
+starting the shell, you can also add a mode hook to set
+`proof-eagerly-raise' e.g.:
+  
+  (add-hook 'proof-goals-mode-hook 
+    (lambda () (setq proof-eagerly-raise nil)))
+  (add-hook 'proof-response-mode-hook 
+    (lambda () (setq proof-eagerly-raise nil)))
+
+This causes the previous behaviour as in PG 3.4: frames are only
+created as text is displayed in them.  (This is the default for
+the trace buffer).
+
+Generally, the best way of working with multiple frames is to try not
+to stop/start the proof assistant too much (this involves killing
+buffers, which spoils the frame/buffer correspondence).
+
+If you find other particularly annoying behaviour, please do report
+it, but give a careful description of how to reproduce, what happened,
+and what you expected to happen.  Probably you will just have to work
+around the issue.  For future versions of PG the multiple frame
+handling code will probably be custom written (rather than using
+`special-display-regexps').
+
 ** Toolbar enablers unreliable on some platforms.
 
 Occasionally the buttons are disabled/enabled when they shouldn't be.