From 68a34024d20d1684baebb7015b8f81e70234db95 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Wed, 6 Oct 1999 11:39:35 +0000 Subject: Updated --- todo | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/todo b/todo index 5bdbf99f..2ba6da46 100644 --- a/todo +++ b/todo @@ -52,6 +52,26 @@ A Pending work, in progress [da]: re-enabled), proof-toggle-scripting, new configuration options. proof-cd +B After interrupt, queue region is left intact. Seems odd. + Let's remove it. + +B bug: interrupting Isabelle process sometimes doesn't return, why? + (see first half of interrupt error only: + *** Interrupt. + *** At command "time_use". + + uncaught exception ERROR + raised at: library.ML:1100.35-1100.40 + But not "uncaught exception" part. + What is worse: prompt disappears! But process still seems to be + there underneath. Not sure where this bug comes from. + + Moreover, killing process then hangs Emacs with message + "cleaning up", and get error + (1) (error/warning) Error in process sentinel: (no-catch exited t) + +C Add new test cases for closure of unfinished proofs in Lego, + Isabelle. C Usability enhancement: Movement of point after assert/retract commands -- cgit v1.2.3