From 69dcecfc6b8a30b95d5ed6b9d93e4c25878a06b6 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 16 Dec 1998 15:31:21 +0000
Subject: Removed suspected bug mentioned by David von O.  Now assumed to be
 due to his own hacking of Proof General. Added proof-shell-exit item
 concerning the time delay built-in.

---
 todo | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

diff --git a/todo b/todo
index 381d06f2..7a188db2 100644
--- a/todo
+++ b/todo
@@ -35,10 +35,6 @@ and output as usual?   (The effect would be to allow Isabelle's
 completed proof message to appear in the goals buffer since it's
 marked up as a proof state output)
 
-A*** Possible bug [Isabelle/all]:
- at the top of a script buffer, sometimes special commands like
- ProofGeneral.kill_goal(); are inserted without reason
-
 A*** catch bug on Solaris when process shell killed?
 
 
@@ -53,6 +49,13 @@ A Polish ProofGeneral.texi and publish LaTeX version as an LFCS
    * Fixup markup mistakes by editing docstrings.
    * Fix docstring magic so PROOFGENERAL_HOME is not var'd.
 
+B proof-shell-exit has a time delay of 10 secs built-in, 
+  before which the process is killed off.  
+  This should be configurable to allow for proof assistants 
+  which really want to do some work before exiting, for
+  example writing persistent databases out or the like.
+  Also this fact should be documented.
+
 B Is it possible to let C-c C-c (SIGINT) issue additional process input?
   Poly/ML requires an 'f' at the interrupt handler's prompt to proceed, or
   rather, to fail gracefully.
-- 
cgit v1.2.3