From 6b5b8cc1fc9ae35ca37a0db4ae82dd1fb5b74851 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Fri, 31 Aug 2001 11:37:43 +0000 Subject: Remove minibuffer bug --- BUGS | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) (limited to 'BUGS') diff --git a/BUGS b/BUGS index d148133a..f230ab8b 100644 --- a/BUGS +++ b/BUGS @@ -15,6 +15,11 @@ versions, and those which only apply to particular versions. * Generic problems, for all Emacs versions +** Visibility control doesn't distinguish theorems with same name. + +If you have more than one theorem with the same name in a buffer, +their proof visibilities are controlled together. + ** If the proof assistant goes into a loop displaying lots of information It may be difficult or impossible to interrupt it, because Emacs @@ -23,7 +28,8 @@ push (or anything else). In this situation, you will need to send an interrupt to the (e.g.) Isabelle process from another shell. If that doesn't stop things, you can try 'kill -FPE '. This problem can happen with looping rewrite rules in the Isabelle -simplifier, when tracing rewriting. +simplifier, when tracing rewriting. It seems to be worse on +certain architectures, and slower machines. ** Toolbar enablers for XEmacs 21, some artefacts. @@ -65,13 +71,6 @@ simplifier, when tracing rewriting. Workaround: manually bind C-c RET to 'proof-goto-point instead. -** Active minibuffer can cause strange buffer selection behaviour. - -Try this: start PG/isar, step into a proof, activate a mini buffer (by -visit-file etc.), now update goals output by clicking the toolbar. PG -will attempt to put the output into the minibuffer portion of the -frame! To get back to a sane state, use C-] - * Problems with particular Emacs versions ** Emacs menus: options not updated dynamically, positions erratic, etc. -- cgit v1.2.3