From ce89a51140af9b7bacaedf90dfeebc7313b4eea9 Mon Sep 17 00:00:00 2001 From: Thomas Kleymann Date: Thu, 10 Sep 1998 15:08:51 +0000 Subject: Reengineering efforts to exploit 3 buffer model now top priority --- todo | 24 ++++++++++++++++-------- 1 file changed, 16 insertions(+), 8 deletions(-) diff --git a/todo b/todo index 177099d1..5d2ba58d 100644 --- a/todo +++ b/todo @@ -140,8 +140,8 @@ B Introduce keybinding to save the proof e.g., in LEGO, this should B Unify toolbar and menu functions. -D use proof buffer instead of response buffer and leave non-proof - state output in the process buffer (1h) +A use proof buffer instead of response buffer and leave non-proof + state output in the process buffer (2h tms) D Remove duplication of variables e.g., proof-prog-name and lego-prog-name for Coq and Lego. (1h) @@ -179,12 +179,6 @@ X pbp code doesn't quite accord with the tech report; in particular it A fix Pbp implementation (10h; tms) -X Mechanism to save object file - -B Equiv, Next,... aren't handled properly, because LEGO does not - refresh the proof state. Perhaps it would be easiest to get LEGO to - output more information in proof script mode (2h tms) - A Error messages need to be revised e.g., if an import fails, LEGO outputs @@ -196,6 +190,20 @@ A Error messages need to be revised e.g., if an import fails, LEGO A release new version of the LEGO proof engine (4h tms) +B Equiv, Next,... aren't handled properly, because LEGO does not + refresh the proof state. Perhaps it would be easiest to get LEGO to + output more information in proof script mode (2h tms) + +B LEGO should not issue warning messages triggered by the interactive + use of the Module command when invoked by the interface e.g., + + Lego> Module nstderror Import stderror; + Including module nstderror + Warning: module name "nstderror" does not equal filename ""! + Warning: Interactive use of Module command. + +X Mechanism to save object file + * Here are things to be done to Coq mode ======================================== -- cgit v1.2.3