diff options
| -rw-r--r-- | todo | 54 |
1 files changed, 25 insertions, 29 deletions
@@ -14,7 +14,9 @@ X (Low) probably not worth wasting time on ==================================================================== B Revise ProofGeneral.texi and publish LaTeX version as an LFCS - Technical Report + Technical Report (2 days; da + tms) + +B Provide a sensible default frame/buffer layout (4h) C Improve proof-goal-command and proof-save-command: `proof-goal-command' should be more flexible and support a @@ -39,19 +41,21 @@ C Investigate and improve indentation/font-locking code. *very* slow. Moreover the indentation is screwy. Also seems screwy in LEGO/Coq PG. (da, 2hr) -B Add support for people typing directly into the inferior process. - The error messages are going to drive experienced Isabelle users - mad otherwise! Fair enough to hide the buffer from those - dumb users "not authorized for this information", but lets not - get in the way of experienced users. - (da, 1hr: I'm not sure of the best way of doing this) +B New buffer model: + + 1. Script buffers + 2. Response buffer + 3. (optionally part of response buffer) goals buffer + 4. (hidden) process buffer + 5. Minibuffer for additionally sending information to the process B proof-toolbar: Fixup movement of point (choice of up and down functions). Add toolbar to response mode too. (30mins, da) -B toolbar icons: Fixup for low-colour modes again. Improve restart - and qed icon (30mins, da). +B toolbar icons: Fixup for low-colour modes again. (30mins, da). + +B Split code; particularyly proof.el C toolbar icons: Automatically generate reduced and pressed/greyed-out versions from gimp xcf files. Keep the @@ -79,13 +83,13 @@ C User-level functions: C Write test schedule for things to try out with a new instantiation of Proof General. -C Add skeleton instantiation files for a dummy prover "myassistant" to +B Add skeleton instantiation files for a dummy prover "myassistant" to make it easier to add support for new assistants -- looking at any of the existing modes is confusing because of the prover-specific stuff. Ideally it should work for one of the default provers as an impoverished example mode. (2h) -X Add support for putting a locked region in processed files. +A Add support for putting a locked region in processed files. X Make process handling smarter: because Emacs is single-threaded, no process output can be dealt with when we are running some @@ -97,7 +101,7 @@ X Make process handling smarter: because Emacs is single-threaded, we have to wait until something becomes blue to undo it by sending a command to the process. -B Clean up proof-assert-until-point behaviour. At the moment we +A Clean up proof-assert-until-point behaviour. At the moment we get an odd error if it is run in the locked region. If point is on the start of a command it says "nothing to do", but if it is one character into the command, it asserts the whole command! @@ -129,7 +133,7 @@ D Add support to proof.el for *not* setting variables for D Outsource script management features from proof.el to proof-script.el (1h) -B Write function proof-retract-file. (30min tms) +A Write function proof-retract-file. (30min tms) Currently, the command ForgetMark (for LEGO) is hardwired in proof-steal-process. @@ -152,7 +156,7 @@ B Update source documentation and manual, in particular document bugs D Technical documentation to record expertise and allow users of other proof systems to adopt generic package (40h h) -B Implement more generic mechanism for large undos (2h tms) +A Implement more generic mechanism for large undos (2h tms) COQ: C-c u inside a Section should reset the whole section, then redo defns @@ -160,7 +164,7 @@ B Implement more generic mechanism for large undos (2h tms) LEGO: consider Discharge; perhaps unrol to the beginning of the module? -B Multiple files are sometimes handled incorrectly, because the +A Multiple files are sometimes handled incorrectly, because the function `proof-steal-process' cannot figure out that some files have already been processed. This is most likely caused by the ad-hoc equality test on file names. Instead, one could employ @@ -181,7 +185,7 @@ B file handling could be more robust; perhaps one should always cd to achieved with a hook which is not set by default. [Remember to add user documentation] (30min tms) -B replace (current-buffer) by proof-shell-buffer/proof-script-buffer +A replace (current-buffer) by proof-shell-buffer/proof-script-buffer where ever possible (30 min tms) B Reengineer *-count-undos and *-find-and-forget at generic level @@ -216,7 +220,7 @@ X Comment support is not very generic: we don't support end-of-line terminated comments. Is there any case where this might be worthwhile? (2h to add it). -C Make completion more generic. For Isabelle we can build a +C Make completion more generic. For Isabelle and Lego, we can build a completion table by querying the process, which is better than messing with tags. @@ -240,7 +244,7 @@ X Ideas for efficiency improvements. Rather than repeatedly B Change proof by pointing (pbp) stuff into proofstate buffer stuff. -B Fixing up errors caused by pbp-generated commands; currently, script +C Fixing up errors caused by pbp-generated commands; currently, script management unwisely assumes that pbp commands cannot fail (2h) B Rename pbp-mode to response-mode or goals-mode (which doesn't @@ -259,9 +263,9 @@ X pbp code doesn't quite accord with the tech report; in particular it * Here are things to be done to Lego mode ========================================= -B fix Pbp implementation (10h) +C fix Pbp implementation (10h) -B release new version of the LEGO proof engine (4h tms) +A release new version of the LEGO proof engine (4h tms) C Equiv, Next,... aren't handled properly, because LEGO does not refresh the proof state. Perhaps it would be easiest to get LEGO to @@ -373,14 +377,6 @@ D The proof-locked-span isn't set to read-only, because overlays don't B validate/fix web pages. -B remove CVS history in all files (replace with idents $Id) - -B extend Copyright to 1998 - -B fix INSTALL file, add COPYING note - -B fix branches after renames - -B write Makefile targets to build documentation formats, .elc +B add COPYING note B write release message
\ No newline at end of file |