From 4561860fbd1c04e85ebd9dee1c6fba4344c2f30f Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Mon, 29 Nov 1999 13:17:48 +0000
Subject: Note about proof_timing in Isabelle

---
 BUGS | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/BUGS b/BUGS
index 6a8ce17d..3771b5df 100644
--- a/BUGS
+++ b/BUGS
@@ -144,6 +144,11 @@ to proofgen@dcs.ed.ac.uk.
 Isabelle Proof General Bugs
 ===========================
 
+* set proof_timing is problematic: it will make the goals display
+disappear during proof.  This is because Proof General only displays
+goals output that appears *after* Isabelle messages, but Isabelle
+prints the timing message after the goals are displayed.
+
 * There is a general difficulty with proof scripts containing ML
 structures, functions, etc.  Proof General does not understand full ML
 syntax(!), so it will be confused by structures which contain 
-- 
cgit v1.2.3